Remove TABs from examples

src/num/theories/SingleStep.{sig,sml} is gone. The
defininitions of Cases, Cases_on, Induct, Induct_on,
CASE_TAC (and co.) are now in basicProof/BasicProvers.
completeInduct_on and measureInduct_on are now in
numLib. recInduct is now in src/tfl/Induction.sml.
All these are collected in bossLib, so the changes
should be invisible to ordinary users.

SingleStep.*.doc has been changed accordingly.

BasicProvers.NORM_TAC should now automatically perform
all case splits (from if-then-else expressions as
well as case expression) arising anywhere in the goal.

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!

Fix up some minor syntax things that are
now out of date.

Refine front-end outputs to be more consistent with Magnus's backend.

Connect the front-end and back-end of the software compiler.
More refinements are needed for the arm backend to work.

Updates on the software compiler:
1. Extend the front-end to handle polymorphism and higher order functions
2. Add primitive approaches to deal with pattern matching
3. Implement function calls in a caller save style
4. Fix a few bugs in existing source code

Trivial changes to regAlloc. Still working on
getting end-to-end compiler to work.

Added compileDefine, which deals with some ARM peculiarities,
such as small immediate constants, and also tries
to get functions into the particular form needed
by Magnus' backend.

Customize the front-end to produce code in a format the ARM backend needs

Main change:
Register allocation and recursive calls. The registers/memory
locations in all recursive calls have to be the same, e.g.

f(r0,r1) =
if .... then ... f(r0,r1)
else .... f (r0,r1)

This revision is suboptimal however.

A new test file "refined_format.sml" is added to illustrate the results

Updates at the front-end

wrap up compiler 2

Enhancement in the front-end

*** empty log message ***

Revisions, mainly to add machine words and their operations to the
source language.

Revised build so that system can be separately compiled. Also moved
test programs to separate directory.

*** empty log message ***

A blank new implementation of the software compiler