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

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

Up to core types

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

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

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.

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.