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

Upgraded references to UNBETA_CONV and mk_abs_CONV (both essentially the
same function) and removed implementations because of provision of this
function in Conv.

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.

Cleaned up behaviour on Pugh's nightmare example with a partly principled
hack, and also provided my own version of strip_exists to keep me from
getting too confused. Of course, once STRIP_QUANT_CONV is implemented
in terms of GEN_ABS then I will start getting confused again. Provided
a couple of extra little helper functions for manipulating range
constraints.

Moved a couple of useful functions into CooperSyntax (in fact, I think
they are both useful enough to possibly make it into bool/; the
functions are UNBETA_CONV and find_free_terms), and implemented handling
of natural number DIV and MOD (along with test case demonstrating this).

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.

A slew of further changes, including the factoring of some of Cooper.sml
into separate files. Now solves Homeier's SUNRISE problem in just over
30 seconds.