Implement more of Basis2002 for Moscow ML (adding Vector, Array,
ArraySlice and VectorSlice), simplifying what Poly/ML has to emulate.
Haven't done full rebuild test, but have got as far as integerTheory
and Omega, which makes heavy uses of Vector etc.

More corrections required to our sources when I do the migration to
Basis 97 properly.

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.