saving before an update

Revert "upgrading termination condition extractor to handle monadic definitions"

This reverts commit c0256f576177c1fb8a02fc66f665c56e07f1a27d.

upgrading termination condition extractor to handle monadic definitions

miscellaneous fixes

fixed Scott's TFL bug on tc-extraction for higher order combinators like pair_cmp.

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.

Fixes for another problem with calling
Define on literal patterns. Now

Define `(foo (2,3) = 5) /\
(foo (2,4) = 6) /\
(foo (3,6) = 9)`;

is handled.

Implement ML code generation for large records.

Fix to bug spotted by Anthony, whereby the induction
theorem for functions defined by pattern-matching
on literals was failing to be proved. Misc.
simplifications to TFL code plus adding "trypluck" to Lib.

Fix to bug spotted by Anthony.

Fix for a Define bug spotted by mjcg. When
dealing with recursive calls under a case,
if variables with certain names (those
starting with v) are bound in the case
pattern then it can happen that variables
generated during pattern matching can be
the same, leading to failed proofs. Totally
obscure, and dealt with properly (I think)
in normal pattern matching. So, a difference
between Pmatch and Functional. The fix is
to invent a class of variables not accepted
by the parser (i.e. starting *v) and to later eliminate
the weird names from any theorems coming out of Hol_defn.

Some other trivial mods made in passing also, plus
tests for the new behaviour.

Also a new conversional, MAP_THM, which applies the
given conversion to the assumptions and conclusion
of the given theorem.

Mods to get examples working again.

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.

Upgrading Define so that it proves more termination goals.
Generates lex. combinations and tries them out, so gets
some more ordinary recursions. Gets all iterated primitive
recursions. Also has been taught about some operations
on words (so recursion from w to w-1w will terminate,
for example).

Let me know of any bugs/slowdowns, etc.

Adding a fast regular expression matcher. Changing old regexp.sml
to live in regexp.naive

Minor editing and also deletion of unfinished example.

Trivial obsessive mods, plus addition of a regular expression matcher.

Fixes to the induction theorems that TFL produces. Changes to recInduct
to reflect this. Other minor changes.

Small changes to get examples running (eta no longer in std_ss).

Minor changes.

Added VAR_EQ_TAC to BasicProvers. It eliminates assumptions of the
form v = M or M = v (provided v doesn't occur as a proper subterm of M).

The other changes are just messing about.

Minor fixes to some TFL examples, and fixed a problem whereby the
attempted definition of a schema would fail on the attempt to add
the schema to the global compset, thus scuttling the whole definition
attempt. Now just a message is emitted and the definition attempt
succeeds.

Final fixes to separate schematic definitions from ordinary ones.
Also, some of the examples have been polished a bit.

Minor changes.

Minor changes.

Basic improvements.

Changes to handle new interface to Defn.tgoal.

Minor upgrades.

Changes to reflect advances in Defn.

Small changes.

Removing binRec until I get the multiset order proof in HOL.

Polishing.

Upgrades.

A general collection of test cases and examples of the application
of Define.