term.ML: add_loose_bnos now returns a list w/o duplicates. pattern.ML: replaced null(loose_bnos t) by loose_bvar(t,0)

Added comment to function "loops".

(binder "Q" p) generates Binder("Q",p,p); it used to be Binder("Q",0,p).

ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them. MT.thy: Deleted extra space in clos_mk.

Removed the "exit 1" calls, since now the Makefile does them.

ROOT.ML: installed new hyp_subst_tac Nat.ML: Changed proof of lessE for new hyp_subst_tac

Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that the maxidx-filed of thms is computed correctly.

Local version of (original) hypsubst: needs no simplifier

Modified proofs for new hyp_subst_tac.

Modified proofs for new hyp_subst_tac, and simplified them.

Received some local definitions from AC_Equiv.thy.

Moved some local definitions to WO6_WO1.ML

Proved if_iff and used it to simplify proof of if_type.

Now the classical sets include UN_E, to avoid calling hyp_subst_tac

Changed proof of domain_ord_iso_map_subset for new hyp_subst_tac

Added Id: line

Deleted call to flexflex_tac

Added Id: line

Recoded with help from Toby to use rewriting instead of the subst rule -- the latter was too slow. But it must resort to the subst rule if the equality contains Vars.

Added comment.

No longer builds the induction structure (from ../Provers/ind.ML)

Loads the local hypsubst.ML. No longer loads ../Provers/ind.ML, which was never used.

Corrected many errors in the dependencies.

Changed comments and timings.

Updated comments.

Set up for new hyp_subst_tac.

Added Id: line

Fixed typo.

Simplified some proofs and made them work for new hyp_subst_tac.

Now sets loadpath.

Gave tighter priorities to SUM and PROD to reduce ambiguities.

Gave tighter priorities to if, napply and the let-forms to reduce ambiguities.

Now sets eta_contract.

Added Id: line

generalized map (%x.x) xs = xs to map (%x.x) = (%xs.xs)

replaced 'arities' by 'instance';

Simplified using pattern replacements. Added the AC example.

New example of AC Equivalences by Krzysztof Grabczewski

New example of AC Equivalences by Krzysztof Grabczewski

Tried the new addss in many proofs, and tidied others involving simplification.

Tried the new addss in a proof.

Defined addss to perform simplification in a claset. Precedence of addcongs is now 4 (to match that of other simplifier infixes)

changed translation of _applC

changed pretty printing of applC

Added comment about why mem_irrefl should not be a safeE.

Tried the new addss in many proofs, and tidied others involving simplification.

Precedence of infixes is now 4 (just above that of :=)

Addition of wrappers for integration with the simplifier. New infixes setwrapper compwrapper addbefore addafter. New function getwrapper. The wrapper is a tactical that is applied to the step tactic. By default it is the identity. Using THEN one can cause other tactics to be tried before or after the step tactic. Other effects are possible using ORELSE, etc.

Defined addss to perform simplification in a claset. Precedence of addcongs is now 4 (to match that of other simplifier infixes)

removed unnecessary parentheses from the generated rules

Simplification: used Logic.occs instead of mem add_term_frees

changed string scanner so that newlines ('\n') are allowed and ignored inside strings

changed syntax of datatype declarations (curried types for constructor parameters)

renamed theorem "apfst" to "apfst_conv" to avoid conflict with function apfst from Pure/library.ML

Corrected faulty reference to Hindley-Milner type inference

Added recursion equations for foldl to list_ss.

Modified If_def to avoid ambiguity.

changed syntax of tuples from <..., ...> to (..., ...)

fixed bug: parent theory wasn't loaded if .thy file was completly read before (regardless of the .ML file)

fixed bug: HOL_build_completed replaced by CHOL_build_completed