1995-07-28 nipkow added section on "Reordering assumptions".
1995-07-28 nipkow added rotate_tac
1995-07-28 paulson changed AC_... to OrdQuant_...
1995-07-28 paulson Version of the proof macros for LaTeX 2.09
1995-07-28 nipkow added rotate_tac.
1995-07-28 paulson Ran expandshort and corrected spelling of Grabczewski
1995-07-28 lcp Ran expandshort and changed spelling of Grabczewski
1995-07-28 lcp Ran expandshort and changed spelling of Grabczewski
1995-07-28 lcp Ran expandshort and changed spelling of Grabczewski
1995-07-28 lcp Ran expandshort and changed spelling of Grabczewski
1995-07-28 lcp Ran expandshort and changed spelling of Grabczewski
1995-07-27 nipkow Added rev_append and rev_rev_ident to list_ss.
1995-07-27 wenzelm minor fix: instance now raises error if witness axioms don't exist;
1995-07-26 lcp Many small changes to make proofs run faster
1995-07-26 lcp Now includes all the AC files
1995-07-26 lcp tidied proof of add_less_mono
1995-07-26 lcp trivial updates to header and bibliography
1995-07-25 lcp Numerous small improvements by KG and LCP
1995-07-25 lcp match_bvs no longer puts a name in the alist if it is null ("")
1995-07-25 lcp Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
1995-07-25 lcp Corrected mixfix declaration of @perm
1995-07-25 lcp Proved perm_length
1995-07-25 lcp Added two final lines to intro_tacsf for mutual recursion
1995-07-25 lcp Old version of mutual induction never worked. Now ensures that
1995-07-25 lcp Changed comments
1995-07-25 lcp Added Part_Int and Part_Collect for inductive definitions
1995-07-25 lcp Includes Sum.thy as a parent for mutual recursion
1995-07-25 lcp now uses proof209.sty
1995-07-25 lcp trivial update
1995-07-25 lcp trivial update
1995-07-25 lcp finally deleted
1995-07-19 nipkow Updated nipkow-prehofer
1995-07-07 clasohm moved mixfix syntax from sign.ML
1995-07-07 clasohm moved mixfix syntax to Syntax/mixfix.ML
1995-07-05 nipkow Added insert_not_empty, UN_empty and UN_insert (to set_ss).
1995-07-03 clasohm added cargs for curried function application
1995-07-03 clasohm removed debugging output
1995-07-03 clasohm remove Old_HOL
1995-07-03 clasohm added comments; fixed a bug; reduced memory usage slightly
1995-06-30 lcp added mention of new theories BT and Perm
1995-06-30 lcp new inductive definition: permutations
1995-06-29 nipkow Renamed some vars.
1995-06-29 lcp fixed comment
1995-06-29 lcp Proof of n_leaves_reflect uses permutative rewriting.
1995-06-29 lcp Added function rev and its properties length_rev, etc.
1995-06-29 regensbu The curried version of HOLCF is now just called HOLCF. The old
1995-06-29 lcp New theory and proofs including preorder, inorder, ..., initially
1995-06-29 clasohm renamed CHOL to HOL
1995-06-29 clasohm renamed CHOL to HOL
1995-06-29 clasohm renamed CHOL to HOL
1995-06-29 clasohm changed 'chol' labels to 'hol'; added a few parentheses
1995-06-29 clasohm changes made by Lawrence Paulson
1995-06-29 nipkow Minimal proof tuning.
1995-06-26 wenzelm added add_trrules_i;
1995-06-26 wenzelm added add_trrules_i;
1995-06-26 wenzelm added extend_trrules_i;
1995-06-23 clasohm added a few comments on ThyInfo
1995-06-23 nipkow Put in direct proof of C-R w/o detour via cd.
1995-06-22 clasohm removed \...\ inside strings
1995-06-22 clasohm changed call of store_thm_db so that it's result is not displayed
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip