src/ZF/simpdata.ML
2001-03-30 ago the one-point rule for bounded quantifiers
2000-09-07 ago tuned ML code (the_context, bind_thms(s));
2000-08-10 ago installation of cancellation simprocs for the integers
1999-09-21 ago Mod because of new solver interface.
1999-01-27 ago new typechecking solver for the simplifier
1998-09-24 ago renamed mk_meta_eq to mk_eq
1998-08-17 ago Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
1998-07-27 ago A few new lemmas by Mark Staples
1998-07-13 ago Huge tidy-up: removal of leading \!\!
1997-11-03 ago isatool fixclasimp;
1997-10-14 ago Added neagtion rules for Ball and Bex.
1997-10-10 ago fixed dots;
1997-06-06 ago Better miniscoping for bounded quantifiers
1997-04-02 ago Uses ZF.thy again, to make that theory usable
1997-01-09 ago Removal of needless "addIs [equality]", etc.
1997-01-07 ago Default rewrite rules for quantification over Collect(A,P)
1997-01-03 ago Implicit simpsets and clasets for FOL and ZF
1996-06-07 ago Addition of converse_iff, domain_converse, range_converse as rewrites
1996-03-26 ago Added new rewrite rules about cons and succ
1996-01-30 ago expanded tabs
1995-04-13 ago Recoded function atomize so that new ways of creating
1995-01-12 ago Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
1994-12-08 ago test_assume_tac: now tries eq_assume_tac on exceptional cases
1994-08-16 ago ZF/pair.ML: moved some definitions here from simpdata.ML
1994-08-12 ago installation of new inductive/datatype sections
1994-07-26 ago Axiom of choice, cardinality results, etc.
1994-07-12 ago new cardinal arithmetic developments
1994-06-21 ago Addition of cardinals and order types, various tidying
1994-03-17 ago Improved layout for inductive defs
1993-09-30 ago ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
1993-09-17 ago Installation of new simplifier for ZF. Deleted all congruence rules not
1993-09-16 ago Initial revision