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

A new routine for doing further normalisation of divisibility terms.

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

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.