2005-08-02 ago simprocs: Simplifier.inherit_bounds;
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-07-30 ago keep type_solver;
2003-01-15 ago more new-style theories
2002-08-06 ago sane interface for simprocs;
2002-01-21 ago new simprules and classical rules
2002-01-12 ago renamed forall_elim_vars_safe to gen_all;
2002-01-11 ago replace gen_all by forall_elim_vars_safe;
2001-12-19 ago separation of the AC part of Main into Main_ZFC, plus a few new lemmas
2001-12-12 ago isatool expandshort;
2001-11-15 ago type_solver_tac: use TCSET' to refer to context of goal state (does
2001-11-15 ago miniscoping of UN and INT
2001-10-05 ago sane spacing of "-";
2001-05-21 ago if_splits and split_if_asm
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