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!

Fixed a subtle bug in termination condition extraction,
whereby multiple let-bindings for a variable would
cause Define to be unpredictable and sometimes broken.
Now variables get renamed in order to make the definition
process succeed. So the definition

Define `field_exp_aux (r5:word32,r6:word32,r7:word32,r10) =
if r6 = 0w then (r7,r10) else
if r6 && 1w = 0w then
let r6 = r6 >>> 1 in
let r2 = r5 in
let r3 = r5 in
let (r4,r10) = field_mult (r2,r3,r10) in
let r5 = r4 in
field_exp_aux (r5:word32,r6:word32,r7:word32,r10)
else
let r6 = r6 >>> 1 in
let r2 = r7 in
let r3 = r5 in
let (r4,r10) = field_mult (r2,r3,r10) in
let r7 = r4 in
let r2 = r5 in
let r3 = r5 in
let (r4,r10) = field_mult (r2,r3,r10) in
let r5 = r4 in
field_exp_aux (r5:word32,r6:word32,r7:word32,r10)`;

will, in the second recursive call, rename r7,r2,r3,r4,r5,r6,
and r10 (twice):

|- field_exp_aux (r5,r6,r7,r10) =
(if r6 = 0w then
(r7,r10)
else
(if r6 && 1w = 0w then
(let r6' = r6 >>> 1 in
let r2 = r5 in
let r3 = r5 in
let (r4,r10') = field_mult (r2,r3,r10) in
let r5' = r4 in
field_exp_aux (r5',r6',r7,r10'))
else
(let r6' = r6 >>> 1 in
let r2 = r7 in
let r3 = r5 in
let (r4,r10') = field_mult (r2,r3,r10) in
let r7' = r4 in
let r2' = r5 in
let r3' = r5 in
let (r4',r10'') = field_mult (r2',r3',r10') in
let r5' = r4' in
field_exp_aux (r5',r6',r7',r10'')))) : thm

Thanks to Magnus for bringing this to my attention.

First version of function definition with constant patterns.
Basic definitions seem to work, but the induction theorems
can be simplified.

- Defn.const_eq_ref := reduceLib.NEQ_CONV;;

Here's the definition of Fibonacci:

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

This yields the definition

> |- (f 0 = 1) /\
(f 1 = 1) /\
(f v = case v of 0 -> 1 || 1 -> 1 || v -> f (v - 1) + f (v - 2)) : thm

which may or may not suit your idea of what should be returned.
It could return a conditional theorem for the last clause of
the definition, but then EVAL would probably not know how
to evaluate it.

The induction theorem is mostly in the right format, although
I wonder if it could be made nicer ..

- val ind = REWRITE_RULE [] (fetch "-" "f_ind");;
> val ind =
|- !P.
P 0 /\ P 1 /\
(!v.
(~(v = 0) /\ ~(v = 1) ==> P (v - 1)) /\
(~(v = 0) /\ ~(v = 1) ==> P (v - 2)) ==> P v)
==>
!v. P v : thm

Here's a more complicated definition (others solicited), which
shows that better post-definition simplification is definitely
needed. But that should be pretty easy to add now that the basics
are working.

Define
`(h (0,0) = T) /\
(h (0,1) = F) /\
(h (1,0) = F) /\
(h (1,1) = T) /\
(h (u,v) = h (u-1, v-1))`;

<<HOL message: mk_functional:
pattern completion has added 2 clauses to the original specification.>>
Equations stored under "h_def".
Induction stored under "h_ind".
> val it =
|- (h (0,0) = case 0 of 0 -> T || 1 -> F || v7 -> h (0 - 1,v7 - 1)) /\
(h (0,1) = case 1 of 0 -> T || 1 -> F || v7 -> h (0 - 1,v7 - 1)) /\
(h (1,0) = case 0 of 0 -> F || 1 -> T || v11 -> h (1 - 1,v11 - 1)) /\
(h (1,1) = case 1 of 0 -> F || 1 -> T || v11 -> h (1 - 1,v11 - 1)) /\
(h (v3,v) =
case v3 of
0 -> (case v of 0 -> T || 1 -> F || v7 -> h (0 - 1,v7 - 1))
|| 1 -> (case v of 0 -> F || 1 -> T || v11 -> h (1 - 1,v11 - 1))
|| v3 -> h (v3 - 1,v - 1)) /\
(h (1,v11) =
case v11 of 0 -> F || 1 -> T || v11' -> h (1 - 1,v11' - 1)) /\
(h (0,v7) = case v7 of 0 -> T || 1 -> F || v7' -> h (0 - 1,v7' - 1))
: thm

Big re-organizational changes. Tfl and tflLib are gone ... the relevant
files are instead Defn and TotalDefn.

Start of a re-organization of the TFL library. The idea is to get rid
of the generality stemming from making it work for both Hol and Isabelle.
Maybe this is a step backwards, but I got sick of all the cruft.

Major changes to accomodate TFL advances. Now mutual, nested, and
schematic recursions can be given. Termination relations can be
deferred for these (in fact, deferred definitions are the only
way of making such definitions currently).

WFScript.sml has been eliminated and its components have been
dispersed to the appropriate theories (pairTheory, prim_recTheory,
and listTheory).

Defn provides a high-level interface to deferred definitions.
Defn relies on very little background support, so it can be
used when one does not need (or desire) the full weight of
bossLib.

Halts has been moved from bossLib.

tflLib may soon go away, since its functionality should in the
longer run be subsumed by Defn + Halts.

Initial revision