Add support for "quot" and "rem" in intSyntax.

Addition of destructors and recognizers for datatypes.
So far, I've just got basic support put in.

Some other trivial mods as well.

LEAST_INT binder added.

Attempt to tidy up (fix) EmitML and finish off the transition that Scott
started. EmitML has been moved to the end of the build sequence. "Hooks"
have been eliminated and all EmitML related stuff has been removed from the
various theory directories. All code for generating ML/Caml is now
self-contained within src/emit. I've not tested the generated Caml code but
the SML seems to build fine.

The directories:

src/theoryML
src/theoryOcaml
src/emitScript

have been replaced by

src/emit/theories/ML
src/emit/theories/Caml
src/emit/theories

Functions for min and max added.

Add some pre-processing code so that the decision procedures can
handle the Num constant, which coerces from integers to natural
numbers. Changes to intSyntax include adding {mk,dest,is}_Num and
also dest_absval.

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

Upgraded int_ss and added MIN and MAX to various simplification
support.

Moved non-integer theories to more appropriate places. Also, this
big re-org. meant that a subtle problem crept in at the beginning
of integerScript, so an obscure hack was needed to set things
right (see the comments about resetting the implicit rewrites
for REWRITE_TAC).

Support for ML evaluation of HOL terms. Preliminary.

Modified to calculate integer remainders and quotients.

Introduced standard triple of {is_,mk_,dest_} for modulus and division
terms over the integers.

Updates to intSyntax and intSimps in order to support a new RED_CONV
function in the interface to intSimps, which applies only to reducible
integer calculations, and raises a HOL_ERR otherwise.
Cooper now includes a counter-example generation sub-function that I
will probably take out because it slows down true goals.

In dividesScript:
* change DIVIDES_REF to be DIVIDES_REFL
* prove DIVIDES_TRANS
In gcdScript:
* eliminate a duplicate copy of GCD_0L
* prove an efficient rewrite for calculating gcds with computeLib
In intSyntax:
* add {mk_,dest_,is_}injected functions
In int_arithScript:
* prove a couple more useful theorems for dealing with gcds
In integerScript:
* prove that x int_divides 1 = (x = 1) \/ (x = ~1)

Added dest_negated function.

Added max_tm.

Added some more dest_ functions.

Upgraded for Kan.0.

Made it all Kananaskis compatible.

Decision procedure now keeps equality terms rather than normalising
them away, and seems a deal quicker as a result, though its
performance on pt7 has worsened by at least a factor of two. This
will bear investigating.

Purely notational changes. I thought the name "COOPER_CONV" would be
catchy ...