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.

New version of Metis:

+ Uses finite models to guide clause selection in resolution.
+ A Metis test for when HOL is compiled using MLton.

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.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.

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