Remove eqtype declaration for term type

Fix & document an infinite loop bug in intSimps.{OMEGA,COOPER}_ss

Problem was that the term F was viewed as suitable context for the
simplifier's decision procedure. Though superficially reasonable, this
leads to problems because the simplifier will rewrite everything it
can inside this context to F, using the rewrite

[F] |- somegenvar = F (1)

but the integer decision procedures will correctly rewrite occurrences
of F to T, because the underlying conversion is happy to prove

|- (F ==> F) <=> T

The natural number procedure in ARITH_ss doesn't suffer from this
problem because it doesn't add F as context to the decision
procedure's context, and that's the fix taken here.

The decision to use (1) above rather than rewrite to true, say, was
taken in 9bc4bdaa.

Fix another compile-time error caused by adoption of generic thy data.

* Make COOPER_ss and OMEGA_ss available in addition to INT_ARITH_ss.
The latter is an alias for OMEGA_ss. They seem to work.
* Fix the svn:ignore property of src/integer/testing

Add an embodiment of the Omega d.p. for use inside the simplifier. It
can perform quite badly on goals with too many disjunctive assumptions
(and ~(x = y) counts as a disjunction).

A whole mess of small changes intended
at making simpsets prettyprint informatively
in the interactive loop. Very possibly
I haven't updated all the files in the examples
directories.

Fix a bug in the normaliser, instantiate it for the integers, and list some
tests for the integer instantiation.

Changed a couple of misleading/annoying names. The type ssdata is now
called ssfrag (to bring it into line with documentation that talks about
simpset fragments), and the constructor SIMPSET is now called SSFRAG.
It never created a simpset, so the latter was a stupid name.

Removed unnecessary infix declarations.

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

INT_REDUCE_ss wasn't reducing ABS terms.

Make calculation (reduction) with the integers an automatic part of the
stateful rewriter.

Cause integer reductions to be added to global compset (for use by
bossLib.EVAL et al), when intSimps is loaded.

Modified to calculate integer remainders and quotients.

Added AC normalisation simpset fragements to intSimps, and removed an
associativity theorem from the standard rewrites exported by integer
theory.

Added handling of absolute value to the integer "compset" (used by
REDUCE_CONV).

Squeezed a little more performance out by using QConv functions in a few
more places.

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.

Added an int_compset : unit -> computeLib.compset function to the
module. This allows people to build on top of the integer reduction
compset without affecting the original value.

More changes supporting the global compset.

Removed a (now) misleading comment.

Reimplemented REDUCE_CONV in intSimps, by making it use computeLib
directly. This should speed it up. Many _REDUCE theorems needed for
this additionally proved in integerScript.sml. int_arithScript has
just had a couple of minor tidy-ups.

Made it all Kananaskis compatible.

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

Added definition of integer minimum and a slew of theorems about integer
divisibility. All needed for Cooper's Presburger decision procedure.

Aargh. & changed its name to int_of_num, and this file didn't know.

I'm doomed to keep on updating this theory. Added a simpset for doing
integer calculations. A decision procedure will have to wait until
someone else decides they really need it.