Remove -- as an alias for Term parser.

As per comment in release notes this has long been replaced as
appropriate style.

Fix ALL_CONV case of FOLDR_CONV; add tests

Fix FOLDR_CONV

Fix listLib.FLAT_CONV

Include some tests.

Closes #358

Reimplement/fix listLib.EL_CONV, providing tests

Closes #357

A slightly more efficient version of ListConv1.FOLDL_CONV.

Faster version of REVERSE_CONV.

Overhaul to rich_listTheory (it had become a bit of a disaster area).

Some points:

1. rich_listTheory now uses the same constant names that are used in listTheory, e.g. TAKE instead of FIRSTN.

2. listTheory theorems are no longer replicated (saved again) in rich_listTheory. This avoids DB.match returning multiple instances of the same theorem. It also avoids saving around 100 theorems twice — in some cases after re-proving them.

3. Compatibility is now maintained though a bunch of SML "val" assignments added using adjoin_to_theory, e.g.

val ZIP_FIRSTN_LEQ = ZIP_TAKE_LEQ
val ALL_DISTINCT_SNOC = listTheory.ALL_DISTINCT_SNOC

4. Some incompatibilities are introduced:

* FRONT___LENGTH is deleted, since it is the same as rich_listTheory.LENGTH_FRONT.
* COUNT_LIST___ADD -> COUNT_LIST_ADD
* COUNT_LIST___COUNT -> COUNT_LIST_COUNT
* The compute theorems for COUNT_LIST and SPLITP have been renamed.
* Some other theorems are no longer saved, e.g. rich_listTheory.list_INDUCT

5. Some theorems in listTheory have gained quantifiers.

Moved GENLIST from rich_list to list.
Also moved some theorems about SNOC and about MAP.

Avoid warning messages when loading listLib under Poly/ML.

Involves adding rich_listSyntax.

Move Thomas' list_eq_simp_ss to listSimps and make it automatic.

This requires the movement of SNOC and some theorems from rich_list to list.
Making the simpset fragment automatic may break proofs by solving more than
expected.

Reimplementation of LIST_EQ_CONV to fix a number of problems. The main problem were terms like
(l1 ++ l2 = l1) or (l1 ++ l2 = l2).

list_eq_simp_ss, a simpset-frag to call LIST_EQ_SIMP_CONV added

NORM_CONS_APPEND_CONV and LIST_EQ_SIMP_CONV added.

These conversions can handle lists that consists of
a combination of
- the empty list ([])
- cons (::)
- append (++)
- SNOC

NORM_CONS_APPEND_CONV brings such lists in normal form.
Example: NORM_CONS_APPEND_CONV converts
``x1::x2::l1 ++ ([] ++ l2 ++ l3) ++ [x3; x4] ++ ([x5] ++ x6::l5)`` to
``x1::x2::(l1 ++ l2 ++ l3 ++ [x3; x4; x5; x6] ++ l5)``

LIST_EQ_SIMP_CONV is intended to simplify equations of lists of removing common parts
on the start and end of the lists.
Example: LIST_EQ_SIMP_CONV converts
``(l1 ++ l2 ++ [x3] ++ l3 = l1 ++ l2' ++ x3'::l3)`` to
``(l2 = l2') /\ (x3 = x3')``

* 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)

Rsyntax is an abomination.

Don't think this code is used much (if at all), but the antiquotation here
breaks with the new filter.

* fix bugs in conversions in ListConv1, which were relying on old style
rich_list names for constants, when these constants have moved to
list, and had their names change too. (Overloading means that the constants
still look as if they have the old names, but they don't really.)
* Make the rich_list names defer to the new ones, even when rich_list is
loaded. You can write ``ALL_EL``, but the system will come back with
``EVERY`` now. No opportunity to discourage use of rich_list is passed
up. :-)

Follow-on fixes to changing Term to Parse.Term and Type to Parse.Type
in the quotation pre-processor. A mass of trivial changes, but the
new way of dealing with files containing code that does parsing
(not script files) is to

* grab the ambient grammar(s)
* set the current grammar(s) to the right values
for parsing quotations in the file
* the body of the file
* reset the current grammar to the ambient grammar

For an example, see src/taut/tautLib.sml

Added type abbreviations for bags (
Added type abbreviations ('a bag, 'a multiset) to bagTheory. Minor
supplements to existing syntax APIs. Fixed a bug in listSyntax.dest_list,
found by Peter Homeier.

Removed dependency on global grammars.

Upgraded to build in Kan. 0.

Made directory Kananaskis compatible; added listSyntax library.

Changes due to the incorporation of John Harrison's datatype definition
package.

This comes from changes to numLib.

Changes to accomodate new look portableML.

Un-dollared + caused this file to fail to load.

Fixed to bring it up to date with Taupo release 0.
(Changes have come across from parse_branch development.)

Initial revision