Fix bug in integer d.p.s' handling of ODD/EVEN.

Include test-case.

Rewriting of ODD now uses

|- ODD n <=> ?m. n = 2 * m + 1

rather than

|- ODD n <=> ~(2 int_divides n)

because in the latter, the elimination of natural number subtraction
can't get to grips with the "isolated" argument n.

Closes #437

Make the integer decision procedures handle maximum and minimum.

This works for :num and :int. In both cases, the treatment is to
expand with the definition of the relevant constant.

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

Bug-fixes and test-cases from problems in src/rational.

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.

Implement improved handling of integer div and mod, along lines already
done for natural number operations. This allows Omega to prove John Matthew's
example, recently posted to the Isabelle mailing list, in half a second.
(Cooper seems to fail miserably.) Added this example (in four variants)
to the test case suite.

Implement some improvements to the pre-processing of natural number goals
such that OMEGA can now prove goals of the form
(x MOD c + y MOD c) MOD c = (x + y) MOD c
in reasonable time. Cooper can't, unfortunately, so the test case for the
above (with c = 1001) is added to a new class of examples that are only
tried for Omega.

Multiplication normalisation bug fixes, along with a couple of extra bugs
picked up along the way recorded in the test cases.

A fix for my "natural number goal" bug. (And a new test case for no
particularly good reason.)

Fix for bug 964085 (to do with DIV/MOD expressions nested inside
themselves). Also made the procedure cope with the presence of
?! quantifiers with scope over DIV/MOD expressions. Added test cases
to demonstrate. Unfortunately, the example I chose in the bug report
above produces a goal that takes too long to solve (the bug was in the
production of the goal), so my exemplar of the bug in the regression
test suite is instead
(x MOD 2) MOD 2 = x MOD 2
which is rather less interesting.

Added a few newlines at end of files to suppress warnings from my
Mosml -> MLton preprocessor.

A fix for the bug reported in hol-info by Arthur van Leeuwen. Also
extended the testing programs to be able to check goals (like the one
he provided as an example).
The problem is that his goal had an assumption where the
non-presburger sub-term was in the scope of a universal quantifier.
(If it was a existential then it could be pulled out, turned into a
universal, stripped, allowing access to the non-presburger sub-term
so that it could be generalised away.) The conversion still doesn't
cope with this situation, but the tactics now won't attempt to include
assumptions that look like that.

Got rid of QConv, and made all conversions do the "raise exception to
indicate reflexivity" thing. (Also fixed bug in new implementation
of ABS_CONV that attempted renaming on failure of conv, and not just
failure of ABS.)

Next step will be to rework the simplifier's implementation so that
it also uses Conv.UNCHANGED, rather than in its own internal version
of the same. This will let the simplifier play efficiently with
others.

May also assess making ABS_CONV not do renaming, and give the rewriter
its own special traverser. This might make some things more efficient.

{COOPER,OMEGA}_TAC now both try to use the assumptions when they run.
They're no longer just CONV_TAC {COOPER,OMEGA}_CONV. The new implementation
moves all assumptions whose non-Presburger sub-terms have type :int or :num
onto the goal, and then calls CONV_TAC.

Added some test cases due originally to JRH (via Konrad) and discovered
a bug in Cooper's handling of conditional expressions. Fixed the
problem by making some code from IntDP_Munge visible.

Konrad found a bug: elimination of subtraction has to happen after DIV
and MOD are eliminated so that terms of the form (x - y) DIV c are
handled properly. Added a couple of test cases to demonstrate the bug
in the old version.

Improvements to the decision procedures. Omega is now somewhat smarter
about doing useful work before throwing itself into DNF-ication.
I think there are probably one or two more optimisations to be done
along these lines.

Moved handling of integer division (mod) problems into IntDP_Munge.

Progress with Omega. Also refactored code for handling natural numbers
and generalising over non-presburger sub-terms so that both Omega and
Cooper can use it.