Add SUC_RULE.

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.

Move ARITH_NORM_ss to numSimps.

Add a new arithmetic normalisation simpset fragment to numLib.

Eventual intention is to have this as part of the stateful rewriting simpset
where it will break lots of proofs until I either fix them, or just 'diminish'
the simpset at the head of the broken scripts.

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.

This check-in mainly fixes a problem with
literals occurring in patterns of TFL-style
definitions. There are a host of other minor
changes as well.

New LEAST_ELIM_TAC for dealing with goals that include LEAST-terms.

Added new higher order rewrite rule for bounded quantifications. This
addition is for existentials; bounded universals were checked in a while
ago. Conversions have been added to numLib, since the simplifier didn't
seem to do the "right thing" with these theorems.

Many small changes, most associated with boolification or lifting.

Implement some useful code to transfrom SUC-based definitions into ones
that can be used with numerals easily (no conditional rewrites necessary).

Added new facilities for dropping or preferring certain numeric types
all at once. Documented one of the new functions, and fixed the
documentation for add_numeral_form, which now automatically adds the
appropriate overloading for "&" (I realised that we didn't need to
force the user to do this themselves).

Minor changes

NonRecSize - fixed problem that "bool_case 0 0" is ambiguous depending
on what "0" is resolved to.

Addition of SUC_ELIM_CONV, from arithmeticTheory, where it was
being adjoined.

Change to structure of numLib so that reduce and arith are incorporated.

Added num_CONV and INDUCT_TAC to numLib for convenience.

Initial revision