Turned some calls to Profile.profile into comments.

Everywhere remove use of temp_set_grammars idiom for setting up the
local grammars, preferring instead to statically bind the appropriate
names. You need to grab Parse.Term and Parse.Type as well as Term and
Type, requiring the definition of a Parse structure.

Add an embodiment of the Omega d.p. for use inside the simplifier. It
can perform quite badly on goals with too many disjunctive assumptions
(and ~(x = y) counts as a disjunction).

I think this is a bug-fix. Now the SEND MORE MONEY test case takes
four hours to raise an exception instead of just a minute. I've taken
it out of the test cases list. I can't easily come up with a test
case that proves this is a bug, but it seems plausible that it is.
(Now I'm going to have to implement that "combine with DPLL d.p.")

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

Made a bunch of changes to the HOL source to make it more "Standard ML",
to make it easier to port to MLton.

For example:
+ Added lots of structure wrappers around miscellaneous .sml files.
+ The type of "before" is 'a * () -> 'a, not 'a * 'b -> 'a, as Moscow ML
currently thinks.
+ Added "val _ = " before random declarations.

A plea: if I'm ever going to succeed in porting HOL to MLton, could
people please stop using Polyhash. It's very useful, but there's
nothing like it in MLton (or indeed Standard ML). In theory I'm going
to have to change the (sometimes complicated) code to use Binarymap or
something like it, but in practice I'll only do that when there's
absolutely no other way.

Added a few newlines at end of files to suppress warnings from my
Mosml -> MLton preprocessor.

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.

Typo correction.

Improved implementation of gcd in CooperMath, thanks to a suggestion of
Ken's. Extended MANIFEST to more accurately reflect the directory.
Removed OmegaTest, which never had any code in it.

Libraries MUST use local parsers, NOT the global one.

A new routine for doing further normalisation of divisibility terms.

Fixed so that gcd correctly handles zero as an argument.

Fixed a bug that was causing this code to fail to simplify things like
2 int_divides 4 * x + 6 * y

Fixed a couple of bugs and added a problem that exhibited one of them
to the regression test suite.

More tweaks and fiddles. The Pugh example now goes through in a reasonable
length of time (same as SUNRISE problem, perhaps a 20-fold speed-up). Also
added a couple of new theorems to integerTheory which will be the basis
for extending COOPER_CONV to cope with division and modulus (as long as
the divisor is a constant).

Further, relatively minor changes in order to get it to go that bit
faster. Pugh's example is still not all it should be, but it seems
that one of the things I'm going to need to do to fix this is get
a fast conversion for pushing ?x. P x \/ Q x \/ R x \/ .. \/ Z x
into a disjunction of existentially quantified clauses. The following
fun push_one_exists_over_many_disjs tm =
((EXISTS_OR_CONV THENC RAND_CONV push_one_exists_over_many_disjs) ORELSEC
ALL_CONV) tm
is *really* slow (= 60 seconds with 120 disjuncts).

Squeezed a little more performance out by using QConv functions in a few
more places.

Total reorganisation of Cooper code. Two ..Core modules can be swapped
in and out of CooperShell to provide "shadow syntax" or my original
implementation of the core phases of the algorithm. Code currently littered
with profiler guff.

Many modifications, based around the last delta-expansion optimisation
from Cooper's paper. In a purely existential goal, there is no
disjunctive expansion until all quantifiers have been eliminated.

Not going to change this anymore. Instead I'm going to write about how
well it performs. Many improvements since last time, and a little
more code factorisation as well. Code should be easy to adjust to
use full gcd optimisations in future for pure goals.