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.

Clean up some METIS library syntax (semantically a no-op)

Mostly deleting redundant infix declarations, but some other random
reformatting along the way

Isolate assignment to traces ref in metis code

Hide assignment to this reference behind add_trace and set_traces
function calls.

Added some extra profiling to see how many primitive inferences Metis
is using in the current version of HOL. If anyone is interested, the
result is:

Goals = 1136
Norm = 2250784 (78%)
Proof = 629622 (22%)
-------------------------
Total = 2880406

I was led to the problem with tautLib.TAUT from this file, which ultimately
wasn't at fault in the bug I was tracking, but which should still have
its local grammars set anyway.

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

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.

New version of the tool suite to port HOL4 to MLton.

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

Rationalized equality axioms for higher-order mode.

Latest version of METIS_TAC.

The biggest change is that scheduling provers is done by number of
inferences, not time used, so METIS_TAC is now completely
deterministic. If it works for you on a subgoal, it will work every
time HOL4 is built.

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.

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.

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.