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.

Omega now passes all of its tests, and I claim it's probably now a reasonable
approximation of a complete procedure for doing Preburger arithmetic.
Aggressive preprocessing attempts to minimise DNF blowup, but the fact
that EXISTS_OR_CONV can still consume over 10% of the procedure's running
time basically sucks.

Omega now works on all of the test case, bar KXSDIV1, on which it
blows up. Some investigation suggests that this is "just" an efficiency
issue and not one of code correctness. With luck, I'll check in some
efficiency changes tomorrow, and then I'll be done.

OMEGA_CONV is now "almost complete". There are just bugs to be ironed out.
Changes are too many to document extensively. Some though:
* OmegaMath has got a lot bigger, with OmegaEq being merged into it and
also gaining some divisibility normalisation code.
* couple of new test cases
* decided against prenexing mixed quantifier problems.

Moved very useful leaf_normalise function into the OmegaMath "library".

Correctly implementing the second optimisation from Friday carves 50s
off the running time for the evil SUNRISE1 test case. (Every test
suite should have such horrors.)

Implemented two more optimisations for "simple Omega". One made
the noxious SUNRISE example go twice as fast. (It's still almost three
times faster if you use Cooper though.)

The first optimisation made the contextual simplification smarter, while the
second took the opportunity to do single-point elimination before converting
to DNF where possible.

Improvements to the decision procedures. Omega is now somewhat smarter
about doing useful work before throwing itself into DNF-ication.
I think there are probably one or two more optimisations to be done
along these lines.

Revisions to the code that DNF-ifies the problem set, including a phase
of "congruential simplification". On those problems that Omega can get
it seems quicker than Cooper in almost all case. One very notable
exception suggests that there is still work to be done though.

Tests revealed that it was much better to let the Canon functions remove
implications and bi-implications themselves rather than doing this first.
Also publish the useful dealwith_nats function from IntDP_Munge.

Progress with Omega. Also refactored code for handling natural numbers
and generalising over non-presburger sub-terms so that both Omega and
Cooper can use it.