Change "thm-names" (used in various places) to be Thy-Name record

This saves on pulling things apart and looking for dots and the like.
It changes the simpLib API (most significantly for the SSFRAG function
which builds simpset fragments).

Fixed normalForms due to "tight equality" changes, moving some test cases into selftest.sml

Make equality of "tight" precedence by default

Start to work through knock-on effects of this.

Give theorems names in simpsets

This is to allow them to be removed easily. System builds on -t1, but
there are still two things to be done

1. the names associated with export_rewrites calls aren't passed on to
the simpsets yet
2. there is not yet an API for removing them

Also, perhaps just as an interim measure, I removed the unused
entrypoint for removing rewrites by pattern matching against their
LHSes (simpLib.remove_theorems).

Remove Globals.priming.

Also remove references to it in code that isn't being tested in the
regression checking build-sequence, and so is probably bit-rotted.

Provide numvariant version of variant, which behaves like

with_flag(Globals.priming,SOME "") (variant avoids)

Document change/incompatibility in release notes.

Make minor (semantically no-op) cleanups in src/metis

Label assignments (v := e) as (* OK *) in src/metis

These labels are my judgement that the references are strictly local
and so not a concurrency issue. Additionally, some assignments in
comments (to Moscow ML specific quietdec, for example) have just been
deleted.

Remove eqtype declaration for term type

Cleanup more code assuming too much of term equality (in metis)

Remove "C" from combinTheory.combin_grammars

Currently, combinTheory is set up to hide C from the global grammar when
it is loaded, but to leave C in combinTheory's own grammar, which you
get via writing things like combinTheory.combin_grammars. This is weird.
To make things more consistent, pull C out of combin's grammar
properly (without having to use adjoin_to_sml), and have it absent in
both descendants, and in combin_grammars.

Of course, the standard trick of typing

reveal "C"

makes it visible again.

The code in src/metis/normalForms.sml used this visibility when stating
and proving a rewrite about C. This was fixed simply by making the
statement use the combin$C notation.

Fix use of integers where it was possible to get them to Overflow.
Use Arbint instead.

A whole mess of small changes intended
at making simpsets prettyprint informatively
in the interactive loop. Very possibly
I haven't updated all the files in the examples
directories.

Update the type of mk_oracle_thm so that it takes a string rather than a
tag as first argument. This is to prevent the following scenario:

- show_tags := true;
> val it = () : unit

- val ax = new_axiom ("foo", ``T``);
> val ax = [oracles: ] [axioms: foo] [] |- T : thm

- val th = mk_oracle_thm (Thm.tag ax) ([], ``F``);
> val th = [oracles: ] [axioms: foo] [] |- F : thm

Changed a couple of misleading/annoying names. The type ssdata is now
called ssfrag (to bring it into line with documentation that talks about
simpset fragments), and the constructor SIMPSET is now called SSFRAG.
It never created a simpset, so the latter was a stupid name.

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

More infix declaration removal.

Improvements to Metis made while investigating bad performance reported
by Anthony, Juliano and Mike.

Bad equality!

New treatment of abbreviations. Documentation still to be updated.
Backwards compatibility illustrated in examples/lambda/standardisationScript
and examples/arm6. New techniques and entry-points illustrated in
core distribution and some of the lambda example scripts.

METIS_TAC now normalizes let terms.

New version of metis: this one actually goes through the compiler
and runs the selftest!

Fixed a bug found by Michael Norrish whereby definitional CNF interacted
badly with type reconstruction. This resulted in some invocations of
METIS_TAC returning "error during proof translation", and then failing to
find a proof with types switched on. All fixed now.

Now that STRIP_TAC has changed, METIS_TAC can safely do pre-normalization
splitting using DISJ_CASES_THEN. The only user-visible result of this
should be better performance.

Fixed a bug discovered by Konrad, where the new version of metis couldn't
prove something the previous version could.

Version 1.3: 17 June 2002

Goals submitted to MESON_TAC when HOL is built .......... 1953
Proved by MESON_TAC ..................................... 1953
Proved by METIS_TAC within 10s .......................... 1946

Between Versions 1.2 and 1.3

* Implemention of definitional CNF to reduce blow-up in number of
clauses (usually caused by nested boolean equivalences).
* Resolution is more robust and efficient, and includes an option
(off by default) for clauses to inherit ordering constraints.

Bug fix: DNF_CONV ``F`` used to yield |-> F = ~T. Oops.

Got rid of QConv, and made all conversions do the "raise exception to
indicate reflexivity" thing. (Also fixed bug in new implementation
of ABS_CONV that attempted renaming on failure of conv, and not just
failure of ABS.)

Next step will be to rework the simplifier's implementation so that
it also uses Conv.UNCHANGED, rather than in its own internal version
of the same. This will let the simplifier play efficiently with
others.

May also assess making ABS_CONV not do renaming, and give the rewriter
its own special traverser. This might make some things more efficient.

Version 1.2: 19 November 2002

Goals submitted to MESON_TAC when HOL is built .......... 1779
Proved by MESON_TAC ..................................... 1779
Proved by METIS_TAC within 10s .......................... 1774

Between Versions 1.1 and 1.2

* Ground-up reimplementation of the resolution calculus, which now
performs ordered resolution and ordered paramodulation.
* A single entry-point METIS_TAC, which uses heuristics to decide
whether to apply FO_METIS_TAC or HO_METIS_TAC.
* {HO|FO}_METIS_TAC both initially operate in typeless mode, and
automatically try again with types if an error occurs during proof
translation.
* Extensionality axiom now included in HO_METIS_TAC by default.

Version 1.1 of the Metis Library.

From the Change Log section of the README:

Between Versions 1.0 and 1.1

* Added a "metis" entry to the HOL trace system: it nows prints
status information during proof (if HOL is in interactive mode).
* Restricted (universal and existential) quantifiers are now
normalized by the NNF conversion.
* (First-order) METIS_TAC can now handle boolean variables.
* Improved performance in the model elimination proof procedure due
to better caching (following a suggestion from John Harrison).
* First-order substitutions are now fully Boultonized.
* The first-order logical kernel makes local tweaks to keep proofs
as small as possible.

Initial check-in of the Metis first-order prover.