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 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
1994-03-17 lcp 1994-03-17 Improved layout for inductive defs
1993-09-30 lcp 1993-09-30 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext domrange/image_subset,vimage_subset: deleted needless premise! misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem ind-syntax/rule_concl: recoded to avoid exceptions intr-elim: now checks conclusions of introduction rules func/fun_disjoint_Un: now uses ex_ex1I list-fn/hd,tl,drop: new simpdata/bquant_simps: new list/list_case_type: restored! bool.thy: changed 1 from a "def" to a translation Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML nat/succ_less_induct: new induction principle arith/add_mono: new results about monotonicity simpdata/mem_simps: removed the ones for succ and cons; added succI1, consI2 to ZF_ss upair/succ_iff: new, for use with simp_tac (cons_iff already existed) ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ nat/nat_0_in_succ: new ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed
1993-09-17 lcp 1993-09-17 Installation of new simplifier for ZF. Deleted all congruence rules not involving local assumptions. NB the congruence rules for Sigma and Pi (dependent type constructions) cause difficulties and are not used by default.
1993-09-16 clasohm 1993-09-16 Initial revision