1996-05-23 berghofe 1996-05-23 Removed equalityI from some proofs (because it is now included in the default claset)
1996-05-23 berghofe 1996-05-23 Replaced fast_tac by Fast_tac (which uses default claset) New rules are now also added to default claset.
1996-05-22 nipkow 1996-05-22 Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
1996-05-22 nipkow 1996-05-22 Added ex_imp
1996-05-22 nipkow 1996-05-22 Added the second half of the W/I correspondence.
1996-05-22 nipkow 1996-05-22 Added swap_prems_rl
1996-05-21 berghofe 1996-05-21 Added additional parent theory equalities because some proofs in Prod.ML depend on rules proved in equalities.ML
1996-05-21 berghofe 1996-05-21 Replaced fast_tac by Fast_tac (which uses default claset) New rules are now also added to default claset.
1996-05-21 nipkow 1996-05-21 Corrected comment wrt I
1996-05-21 nipkow 1996-05-21 Updated url.
1996-05-20 nipkow 1996-05-20 Added thm I_complete_wrt_W to I. Added a few lemmas to Maybe and Type.
1996-05-20 berghofe 1996-05-20 replaced result() by qed "sorted_insort" in last proof
1996-05-17 nipkow 1996-05-17 Added missing default clause | top_const _ = None;
1996-05-17 nipkow 1996-05-17 Added if_image_distrib.
1996-05-17 nipkow 1996-05-17 Had to rename params because variable names in an induction rule changed.
1996-05-17 nipkow 1996-05-17 Moved split_rule et al from ind_syntax.ML to Prod.ML. Used split_rule in Lfp.ML and Trancl.ML.
1996-05-15 paulson 1996-05-15 Deleted spurious line break
1996-05-10 paulson 1996-05-10 Corrected and augmented timings
1996-05-10 paulson 1996-05-10 Updated for new form of induction rules
1996-05-09 paulson 1996-05-09 Updated for new form of induction rules
1996-05-09 paulson 1996-05-09 Removed special syntax for -a-> and nested tuples to left
1996-05-09 paulson 1996-05-09 Updated for new form of induction rules
1996-05-09 paulson 1996-05-09 Added prune_params_tac to improve readability of subgoals
1996-05-08 paulson 1996-05-08 moved ap_split to cartprod.ML
1996-05-08 paulson 1996-05-08 Modified to use new functor signatures
1996-05-08 paulson 1996-05-08 Predicates are now uncurried in both induction rules, regardless of how tuples are nested. Only returns mutual_induct if there is true mutual recursion.
1996-05-08 paulson 1996-05-08 Uses new ap_split from cartprod module
1996-05-08 paulson 1996-05-08 New functor for operating on the two forms of Cartesian product
1996-05-08 paulson 1996-05-08 Added new name cartprod
1996-05-08 paulson 1996-05-08 Updated for new form of induction rules
1996-05-08 paulson 1996-05-08 Updated for new form of induction rules
1996-05-07 paulson 1996-05-07 Updated for new form of induction rules
1996-05-07 paulson 1996-05-07 Removal of special syntax for -a-> and -b->
1996-05-07 paulson 1996-05-07 Unfolding of arbitrarily nested tuples in induction rules
1996-05-07 paulson 1996-05-07 Now split_all_tac works for i>1 !
1996-05-07 berghofe 1996-05-07 Added function claset_of.
1996-05-07 berghofe 1996-05-07 Added function for storing default claset in theory.
1996-05-07 berghofe 1996-05-07 Added functions for default claset.
1996-05-06 berghofe 1996-05-06 Replaced split_tac by split_inside_tac.
1996-05-06 berghofe 1996-05-06 Added split_inside_tac.
1996-05-06 berghofe 1996-05-06 Rewrote mk_cntxt_splitthm. Added function mk_case_split_inside_tac.
1996-05-06 paulson 1996-05-06 Updated timings; more theorems can be proved
1996-05-06 paulson 1996-05-06 Now mentions but does not load mesontest2.ML
1996-05-03 paulson 1996-05-03 updated comments for handling derivations
1996-05-03 paulson 1996-05-03 Extra examples for safe_meson_tac
1996-05-02 paulson 1996-05-02 Restored a proof of Pelletier #38 -- mysteriously deleted
1996-05-02 nipkow 1996-05-02 Added note on types.
1996-05-01 paulson 1996-05-01 Deleted diff_mult_distrib_r as diff_mult_distrib is not proved in Arith.
1996-05-01 paulson 1996-05-01 New cancellation and monotonicity laws, about multiplication and division, from ZF/Arith.
1996-05-01 paulson 1996-05-01 Two new "obvious" examples
1996-05-01 paulson 1996-05-01 Provides merge_cs to support default clasets
1996-05-01 paulson 1996-05-01 Simplified KG's proofs
1996-05-01 paulson 1996-05-01 New lemma inspired by KG
1996-05-01 paulson 1996-05-01 tidied some proofs
1996-04-30 nipkow 1996-04-30 Added an equivalence proof which avoids the use of -n-> (with help from Ranan Fraer)
1996-04-30 nipkow 1996-04-30 Added backwards rtrancl_induct and special versions for pairs.
1996-04-30 clasohm 1996-04-30 changed ident_no_colon so that it forbids postfix "=", too
1996-04-30 clasohm 1996-04-30 changed use_thy's behaviour so that if the user specifies a path for a theory the loadpath is temporarily expanded while the ancestors are loaded
1996-04-30 clasohm 1996-04-30 moved dest_cimplies to drule.ML; added adjust_maxidx
1996-04-30 paulson 1996-04-30 Cosmetic re-ordering of declarations