trailing newlines in *.{sml,sig} files from src/ removed

Trailing newlines from SML files in src/ were rendered in HTML documentation.

Get integer self-test to work with Poly/ML.

Add a test case for Cooper's algorithm corresponding to the

S E N D
+ M O R E
----------
M O N E Y

puzzle. This causes it to break. Don't bother testing it with Omega
as all the inequality constraints would force DNF normalisation to
generate 2^28 clauses. (Hope to fix Cooper in the near future.)

A fix for the bug reported in hol-info by Arthur van Leeuwen. Also
extended the testing programs to be able to check goals (like the one
he provided as an example).
The problem is that his goal had an assumption where the
non-presburger sub-term was in the scope of a universal quantifier.
(If it was a existential then it could be pulled out, turned into a
universal, stripped, allowing access to the non-presburger sub-term
so that it could be generalised away.) The conversion still doesn't
cope with this situation, but the tactics now won't attempt to include
assumptions that look like that.

Reorganised test programs so that regression suite is shared between
omega and cooper tests. Also added useful Perl program for doing
comparisons between test runs.

Removed last vestiges of push_exvar_to_bot, which exposed me to
painful name-choice questions in marked fashion, and also added the
3-5 coins problem to my test suite. I'm still not entirely free of
choice of name problems, and should probably switch back to the built-in
EXISTS_OR_CONV in the meantime.

Testing routine now needs to use DB.fetch.

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

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

Cooper's algorithm now updated to handle mod and div by constants (but
only over the integers for the moment).

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

Added a new problem to test suite (from paper by William Pugh about his
Omega d.p.), but have left it commented out because it's a nasty
pathological case, possibly indicating a bug, or perhaps just pointing
to a really nasty case that Cooper's is doomed to perform badly on.

More reorganisation, mainly to remove listTheory as an ancestory wherever
possible (it still persists as a necessary ancestor of CooperCore, but
isn't used un-necessarily elsewhere).
Also sped up phase5 of CooperCore some more.

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.

A new program to generate integer problems to be fed to Cooper's algorithm
with larger coefficients than the problems generated by the existing
genproblem program.

Added another problem to the standard regression test suite. It seems
to take unacceptably long.

A slew of infrastructure for testing Cooper's algorithm. Useful for
regression testing and efficiency experiments.