Tweak 'using' to now handle unnamed monomorphic theorem arguments

Allow Induct_on & Cases_on to use different theorems with 'using'

The using function is infix on tactics; other tactics can grab 'using'
theorems if they want to try, using the markerLib.maybe_using
entrypoint.

Handle more constants in list_compset

With some regression tests.

Closes #548

Fix pretty-printing of list-forms

Issue was that pretty-printing blocks need to be around the list
delimiters (and included elements), not around just the elements with
the delimiters outermost. The block_info field of the listspec
constructor is now ignored when these are printed; instead the binfo
is lifted (by term_grammar.add_listform) to the rule in which the
listspec appears.

Closes #529

Re-implement Datatype package with TypeBase sexps (not adjoin)

Test EVAL of GENLIST in list selftest

Add regression test for printing of multi-line lists

Make sure recent new constants (from CakeML) are in compsets

In particular, oHD and oEL (aka LLOOKUP need to appear).

Switch order of listform/::-as-infix declarations in listScript

This ensures that list-forms are preferred when possible.

Previously the preference for list-forms was hard-coded into the
pretty-printing code; now the most recent rule is preferred. Of
course, if you write “h::t” that's how it will be printed, as the
listform rule doesn't apply.

Allow list-form syntax to be input with trailing separators

E.g.,

> Datatype `rcd = <| fld1 : num ; fld2 : num list |>`;
<<HOL message: Defined type: "rcd">>
val it = (): unit

> ``<| fld1 := 3; fld2 := [2;3;]; |>``;
val it = “<|fld1 := 3; fld2 := [2; 3]|>”: term

With test-cases over list syntax (implicitly testing
listSyntax.mk_list and some others).

Closes #439

Properly enable case-expr p/printing overloads

This had been made the responsibility of the process that stored
TypeBase information, but that didn't interact properly with the
user-delta approach to storing grammar changes. Now the persistent
overloads are emitted separately.

Add another FOLDR_CONV test

Fix ALL_CONV case of FOLDR_CONV; add tests

Fix listLib.FLAT_CONV

Include some tests.

Closes #358

Reimplement/fix listLib.EL_CONV, providing tests

Closes #357

Fix many selftests to have prettier output

Make listTheory's (short-lived) SINGL constant an overload to ``\x. [x]``

It's nice to have SINGL to hand as an abbreviation for the above
abstraction (particularly as writing the abstraction will usually
require enclosing parentheses, lifting the character count to 9,
compared to SINGL's 5). But one doesn't want to see SINGL 3, when [3]
is so much nicer.

Use the new feature "ignore-for-printing" feature of overload_on (see
ac4806d), so this happens. Somewhat sadly, this does mean that
although one can write MAP SINGL l, one will get back MAP (\x. [x]) l.

Implement "ignore overloads for printing" feature.

Demonstrate with change to list, so that ``~MEM a l`` prints that way
rather than as ``a NOTIN set l``. Selftest checks this, and also that
``x NOTIN {2;3;4}`` continues to print the right way.

Closes #95.

New test demonstrating a bug in LIST_EQ_SIMP_CONV.

* Add TAKE and DROP constants to listTheory, along with a few simple theorems
about them
* Make FIRSTN and BUTFIRSTN in rich_listTheory aliases for the above,
though the constants are now more defined than they were
* Preserve theorem forms in rich_listTheory
* Preserve FIRSTN_CONV and BUTFIRSTN_CONV behaviours (adding selftest too)