src/FOL/simpdata.ML
2011-04-22 wenzelm 2011-04-22 simplified Data signature;
2011-04-22 wenzelm 2011-04-22 misc tuning;
2011-04-22 wenzelm 2011-04-22 modernized Quantifier1 simproc setup;
2011-04-22 wenzelm 2011-04-22 clarified simpset setup; discontinued unused old-style FOL_css;
2010-12-20 wenzelm 2010-12-20 proper identifiers for consts and types;
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-17 haftmann 2010-08-17 more antiquotations
2010-04-30 wenzelm 2010-04-30 removed some old comments;
2010-04-30 wenzelm 2010-04-30 proper context for rule_by_tactic;
2010-04-29 wenzelm 2010-04-29 proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-02-19 wenzelm 2010-02-19 renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-10-17 wenzelm 2009-10-17 explicitly qualify Drule.standard;
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;
2009-07-24 wenzelm 2009-07-24 renamed functor SplitterFun to Splitter, require explicit theory;
2009-07-23 wenzelm 2009-07-23 more @{theory} antiquotations;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-15 wenzelm 2009-07-15 more antiquotations;
2009-07-09 wenzelm 2009-07-09 removed obsolete CVS Ids;
2009-03-20 wenzelm 2009-03-20 Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
2008-09-17 wenzelm 2008-09-17 back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-06-24 wenzelm 2008-06-24 ML_Antiquote.value;
2008-03-29 wenzelm 2008-03-29 purely functional setup of claset/simpset/clasimpset;
2008-03-15 wenzelm 2008-03-15 eliminated out-of-scope proofs (cf. theory IFOL and FOL); proper antiquotations;
2007-04-27 wenzelm 2007-04-27 removed obsolete induct/simp tactic;
2007-01-20 wenzelm 2007-01-20 added @{clasimpset};
2006-11-26 wenzelm 2006-11-26 converted legacy ML scripts;
2006-07-27 wenzelm 2006-07-27 tuned proofs;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-12-31 wenzelm 2005-12-31 removed obsolete Provers/make_elim.ML;
2005-12-01 wenzelm 2005-12-01 unfold_tac: static evaluation of simpset;
2005-10-18 wenzelm 2005-10-18 Simplifier.theory_context;
2005-10-17 wenzelm 2005-10-17 change_claset/simpset; Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-09-12 haftmann 2005-09-12 introduced new-style AList operations
2005-08-02 wenzelm 2005-08-02 simprocs: Simplifier.inherit_bounds;
2005-05-22 wenzelm 2005-05-22 Simplifier already setup in Pure;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2002-08-06 wenzelm 2002-08-06 sane interface for simprocs;
2002-05-15 paulson 2002-05-15 better simplification of trivial existential equalities
2002-01-21 paulson 2002-01-21 new simprules and classical rules
2002-01-15 paulson 2002-01-15 new theorem
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-17 nipkow 2001-12-17 mods due to changed 1-point simprocs (quantifier1).
2001-11-03 wenzelm 2001-11-03 proper use of bind_thm(s);
2001-10-14 wenzelm 2001-10-14 moved rulify to ObjectLogic;
2001-10-14 wenzelm 2001-10-14 eliminated atomize rules;
2001-05-31 oheimb 2001-05-31 streamlined addIffs/delIffs, added warnings
2001-03-29 nipkow 2001-03-29 generalization of 1 point rules for ALL
2000-11-10 wenzelm 2000-11-10 FOL_basic_ss: simprocs moved to FOL_ss;
2000-09-07 wenzelm 2000-09-07 rulify setup;
2000-09-05 wenzelm 2000-09-05 iff declarations moved to clasimp.ML;
2000-08-29 wenzelm 2000-08-29 cong setup now part of Simplifier;
2000-07-13 paulson 2000-07-13 AddIffs now available for FOL, ZF
2000-03-31 wenzelm 2000-03-31 added cong atts;
2000-03-15 wenzelm 2000-03-15 clasimp: include Splitter;
1999-09-21 nipkow 1999-09-21 Mod because of new solver interface.
1999-08-25 wenzelm 1999-08-25 proper bootstrap of IFOL/FOL theories and packages;
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;