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!

Additions to multiset and primeFactor
theories. Fixed definition of PRIMES
sequence in dividesTheory. Also added misc.
theorems to arithmetic. Some amount of
meaningless shuffling about.

Added multiDefine, which can define multiple
functions. If the input is a tangle of
different definitions, it sorts out the
order in which the definitions should be
made. Example:

multiDefine
`(even 0 = T) /\
(even (SUC n) = odd n) /\
(fact x = if x=0 then 1 else mult x (fact (x-1))) /\
(mult x y = x * y) /\
(odd 0 = F) /\
(odd (SUC n) = even n)`;

Overhaul of automated termination prover. It now does a better job
of guessing termination relations, using a relevance criterion
to cut down the number of lexicographic combinations that are tried.
It can handle DIV and MOD now, through the "termination_simps"
variable, which can be added to in order to support other
destructor functions.

Also added DIV_LESS and MOD_LESS to arith_ss. This breaks some proofs,
and I've fixed the broken ones in the standard system build. But there
may still be proofs among the examples directories that will now fail.
If there's a problem with this, I will happily revert.

Support for tDefine.

Revised terminator. Please let me know of any old
termination proofs that no longer go through.

Generalized interface to Define and kin.

Define now handles simple definitions defined by
pattern-matching against (numeric) constants, e.g.

Define `(f 0 = 1) /\ (f 1 = 1) /\ (f n = f (n-1) + f (n-2)`;

But more testing/robustification needs to be done.

Added an API version of Define. Needs some refinement yet. Uses the
"verdict" type

('a,'b) verdict = PASS of 'a | FAIL of 'b

to tell whether a definition attempt succeeded or not (and in which
manner).

Upgrading Define so that it proves more termination goals.
Generates lex. combinations and tries them out, so gets
some more ordinary recursions. Gets all iterated primitive
recursions. Also has been taught about some operations
on words (so recursion from w to w-1w will terminate,
for example).

Let me know of any bugs/slowdowns, etc.

TotalDefn.primDefine now includes the "termination theorem"
in its result.

Big re-org. Have moved the "num" theories gcd and divides to
be with the rest of number theory. SingleStep and TotalDefn
are used in them, so I moved these also into the realm of
numLib. This should make life easier, in general, since
Cases_on, Induct_on, and Define then become usable in
(part of) numLib development.