Remove eqtype declaration for term type

Added once, modified, committed, pushed.
Now re-add, recommit, repush. Sheesh.

Add SUC_RULE.

Implement & use a generic tactic to apply "deep" introduction rules.

A "deep" intro rule is one that looks like

sideconds ==> P (someterm)

The P is a variable and so the P (someterm) pattern can be seen as a
way to match any term that has someterm within it as a sub-term.
Example rules of this form are boolTheory.SELECT_ELIM_THM,
whileTheory.LEAST_ELIM and optionTheory.some_intro. (It's a shame the
names for the older theorems feature "ELIM" as substrings; these are
clearly introduction rules.) We can't use normal first-order
matching, nor higher-order patterns to match such patterns. Instead,
the code performs a search through the term, looking for first-order
matches of someterm.

In both LEAST_ELIM_TAC and SELECT_ELIM_TAC, the search was done by
find_terms; the new implementations of these functions work through
the term in a different, but now well-specified order: top-down,
left-to-right. If there are multiple matches in a term, and it makes
a difference what one you get, you should use DEEP_INTROk_TAC, which
takes a tactic 'continuation'. If this tactic fails with a HOL_ERR
when applied to the resulting goal-state, then DEEP_INTROk_TAC tries
again on a different sub-term, if there is one.

I will write proper documentation for this all shortly.

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.

Follow-on fixes to changing Term to Parse.Term and Type to Parse.Type
in the quotation pre-processor. A mass of trivial changes, but the
new way of dealing with files containing code that does parsing
(not script files) is to

* grab the ambient grammar(s)
* set the current grammar(s) to the right values
for parsing quotations in the file
* the body of the file
* reset the current grammar to the ambient grammar

For an example, see src/taut/tautLib.sml

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.

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.

Added an AC simpset for addition and multiplication. Occasionally useful.

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

Changing arithLib to numLib.

Minor changes

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

paired syntax.

Kananaskis compatibility.

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

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

Minor changes. EXISTS_GREATEST_THM is moved to arithmeticScript
from numLib.

Updated to reflect the fact that libraries need no longer rely on the
contents of the global variables that lurk behind the Term and Type
functions. Instead, they can now use the parse_from_grammars function
and grammar values from theories to make sure that when they parse,
they do so in a known environment.

Added num_CONV and INDUCT_TAC to numLib for convenience.

numLib.sml : performance bug fixed in ADD_CONV

prim_recScript : Basic wellfoundedness theorems about numbers added.

numeralScript.sml : minor tweaks to accomodate change to prim_recScript

NonRecSize : this is a structure that installs `size` functions in
TypeBase.theTypeBase for non-recursive types. This
structure basically keeps sums, products, and options
from depending on nums (and vice versa) in the theory
hierarchy.

Changes to accomodate new look portableML. Change to proof of
DIV_UNIQUE. Addition of some new facts about DIV and MOD (moved
from word/theories/Base.sml).

Old local definition of is_numeral was causing ADD_CONV (and perhaps others)
to fail on reasonable inputs.

Initial revision