src/ZF/simpdata.ML
2011-05-13 wenzelm 2011-05-13 make ZF_cs snapshot after final setup;
2011-04-22 wenzelm 2011-04-22 modernized Quantifier1 simproc setup;
2010-12-20 wenzelm 2010-12-20 proper identifiers for consts and types;
2010-10-28 wenzelm 2010-10-28 discontinued obsolete ML antiquotation @{theory_ref};
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-08-18 haftmann 2010-08-18 more antiquotations
2010-04-29 wenzelm 2010-04-29 proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-03-13 wenzelm 2010-03-13 removed old CVS Ids; tuned headers;
2010-02-28 wenzelm 2010-02-28 more antiquotations; eliminated legacy ML bindings;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2008-03-29 wenzelm 2008-03-29 functional theory setup -- requires linear access;
2007-10-07 wenzelm 2007-10-07 modernized specifications; removed legacy ML bindings;
2007-10-03 wenzelm 2007-10-03 avoid unnamed infixes;
2006-01-21 wenzelm 2006-01-21 removed duplicate type_solver (cf. Tools/typechk.ML);
2005-12-01 wenzelm 2005-12-01 unfold_tac: static evaluation of simpset;
2005-10-17 wenzelm 2005-10-17 change_claset/simpset;
2005-09-12 haftmann 2005-09-12 introduced new-style AList operations
2005-08-02 wenzelm 2005-08-02 simprocs: Simplifier.inherit_bounds;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-07-30 wenzelm 2004-07-30 keep type_solver;
2003-01-15 paulson 2003-01-15 more new-style theories
2002-08-06 wenzelm 2002-08-06 sane interface for simprocs;
2002-01-21 paulson 2002-01-21 new simprules and classical rules
2002-01-12 wenzelm 2002-01-12 renamed forall_elim_vars_safe to gen_all;
2002-01-11 wenzelm 2002-01-11 replace gen_all by forall_elim_vars_safe;
2001-12-19 paulson 2001-12-19 separation of the AC part of Main into Main_ZFC, plus a few new lemmas
2001-12-12 wenzelm 2001-12-12 isatool expandshort;
2001-11-15 wenzelm 2001-11-15 type_solver_tac: use TCSET' to refer to context of goal state (does *not* work with local proof contexts of Isar / new-style locales);
2001-11-15 paulson 2001-11-15 miniscoping of UN and INT
2001-10-05 wenzelm 2001-10-05 sane spacing of "-";
2001-05-21 paulson 2001-05-21 if_splits and split_if_asm
2001-03-30 paulson 2001-03-30 the one-point rule for bounded quantifiers
2000-09-07 wenzelm 2000-09-07 tuned ML code (the_context, bind_thms(s));
2000-08-10 paulson 2000-08-10 installation of cancellation simprocs for the integers
1999-09-21 nipkow 1999-09-21 Mod because of new solver interface.
1999-01-27 paulson 1999-01-27 new typechecking solver for the simplifier
1998-09-24 oheimb 1998-09-24 renamed mk_meta_eq to mk_eq
1998-08-17 paulson 1998-08-17 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy contains fewer theorems than before
1998-07-27 paulson 1998-07-27 A few new lemmas by Mark Staples
1998-07-13 paulson 1998-07-13 Huge tidy-up: removal of leading \!\! addsplits split_tac[split_if] now default nat_succI now included by default
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-14 nipkow 1997-10-14 Added neagtion rules for Ball and Bex. ZF/AC now fails to build. Larry to fix.
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-06-06 paulson 1997-06-06 Better miniscoping for bounded quantifiers
1997-04-02 paulson 1997-04-02 Uses ZF.thy again, to make that theory usable
1997-01-09 paulson 1997-01-09 Removal of needless "addIs [equality]", etc.
1997-01-07 paulson 1997-01-07 Default rewrite rules for quantification over Collect(A,P)
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1996-06-07 paulson 1996-06-07 Addition of converse_iff, domain_converse, range_converse as rewrites
1996-03-26 paulson 1996-03-26 Added new rewrite rules about cons and succ
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-04-13 lcp 1995-04-13 Recoded function atomize so that new ways of creating simplification rules can be added easily.
1995-01-12 lcp 1995-01-12 Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps and UnInt_simps to ZF_ss. Added consI1 to ZF_typechecks.
1994-12-08 lcp 1994-12-08 test_assume_tac: now tries eq_assume_tac on exceptional cases (formulae not of the form a:?A). Affects typechk_tac.
1994-08-16 lcp 1994-08-16 ZF/pair.ML: moved some definitions here from simpdata.ML
1994-08-12 lcp 1994-08-12 installation of new inductive/datatype sections
1994-07-26 lcp 1994-07-26 Axiom of choice, cardinality results, etc.
1994-07-12 lcp 1994-07-12 new cardinal arithmetic developments
1994-06-21 lcp 1994-06-21 Addition of cardinals and order types, various tidying