Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Removed Polyhash

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.

Fixed a bug in the normalisation routine; it wasn't handling the
possibility that it might return ?x. F. New addition to test_cases is
the example that tweaked this bug; thanks to Joe and Konrad for
coming up with it.

Gave OmegaSymbolic a signature file to make it clearer what this module
of the decision procedure does.

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.

Very close to a complete symbolic method.

Moved some theorems about; basic machinery is now in place to decide all
problems with only one sort of quantifier (occasionally the out-of-the-logic
approach breaks, and the symbolic approach is needed, even for all-one-
quantifier problems).

More fiddling (gradual progress) with symbolic implementation of Omega.

More work on symbolic quantifier elimination.

Moved some theorems into the theory file.

Progress with symbolic form of Omega Test.

Initial thoughts on doing Omega the hard way, symbolically.