1995-07-25 ago lcp Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
1995-07-25 ago lcp Corrected mixfix declaration of @perm
1995-07-25 ago lcp Proved perm_length
1995-07-25 ago lcp Added two final lines to intro_tacsf for mutual recursion
1995-07-25 ago lcp Old version of mutual induction never worked. Now ensures that
1995-07-25 ago lcp Changed comments
1995-07-25 ago lcp Added Part_Int and Part_Collect for inductive definitions
1995-07-25 ago lcp Includes Sum.thy as a parent for mutual recursion
1995-07-25 ago lcp now uses proof209.sty
1995-07-25 ago lcp trivial update
1995-07-25 ago lcp trivial update
1995-07-25 ago lcp finally deleted
1995-07-19 ago nipkow Updated nipkow-prehofer
1995-07-07 ago clasohm moved mixfix syntax from sign.ML
1995-07-07 ago clasohm moved mixfix syntax to Syntax/mixfix.ML
1995-07-05 ago nipkow Added insert_not_empty, UN_empty and UN_insert (to set_ss).
1995-07-03 ago clasohm added cargs for curried function application
1995-07-03 ago clasohm removed debugging output
1995-07-03 ago clasohm remove Old_HOL
1995-07-03 ago clasohm added comments; fixed a bug; reduced memory usage slightly
1995-06-30 ago lcp added mention of new theories BT and Perm
1995-06-30 ago lcp new inductive definition: permutations
1995-06-29 ago nipkow Renamed some vars.
1995-06-29 ago lcp fixed comment
1995-06-29 ago lcp Proof of n_leaves_reflect uses permutative rewriting.
1995-06-29 ago lcp Added function rev and its properties length_rev, etc.
1995-06-29 ago regensbu The curried version of HOLCF is now just called HOLCF. The old
1995-06-29 ago lcp New theory and proofs including preorder, inorder, ..., initially
1995-06-29 ago clasohm renamed CHOL to HOL
1995-06-29 ago clasohm renamed CHOL to HOL
1995-06-29 ago clasohm renamed CHOL to HOL
1995-06-29 ago clasohm changed 'chol' labels to 'hol'; added a few parentheses
1995-06-29 ago clasohm changes made by Lawrence Paulson
1995-06-29 ago nipkow Minimal proof tuning.
1995-06-26 ago wenzelm added add_trrules_i;
1995-06-26 ago wenzelm added add_trrules_i;
1995-06-26 ago wenzelm added extend_trrules_i;
1995-06-23 ago clasohm added a few comments on ThyInfo
1995-06-23 ago nipkow Put in direct proof of C-R w/o detour via cd.
1995-06-22 ago clasohm removed \...\ inside strings
1995-06-22 ago clasohm changed call of store_thm_db so that it's result is not displayed
1995-06-22 ago nipkow Simplified the confluence proofs.
1995-06-22 ago nipkow Added add_lessD1
1995-06-21 ago clasohm removed \...\ inside strings
1995-06-21 ago clasohm removed \...\ inside strings
1995-06-21 ago clasohm removed \...\ inside strings
1995-06-21 ago nipkow Added remark that \...\ in strings is unnecessary.
1995-06-14 ago clasohm removed 'raw' productions from gram datatype; replaced mk_gram by add_prods;
1995-06-13 ago clasohm added CHOL
1995-06-12 ago clasohm fixed bug in mfix_to_xprod: lambda productions' lhs shouldn't be modified
1995-06-06 ago lcp converted to LaTeX-2e
1995-06-06 ago lcp Now string_of_vname checks for the empty variable name,
1995-06-02 ago lcp Corrected comments in headers
1995-06-01 ago clasohm commented thms_unifying_with out; placed thm_db into signature again;
1995-06-01 ago nipkow Added dependence on Thy/thm_database.ML
1995-05-31 ago mueller *** empty log message ***
1995-05-31 ago mueller polish
1995-05-30 ago clasohm removed thm_num and thm_db from signature
1995-05-30 ago clasohm fixed bug in thms_containing; changed error/warning messages;
1995-05-30 ago clasohm fixed bug: ThySynFun really shouldn't be deleted