src/FOL/simpdata.ML
2016-08-09 nipkow 2016-08-09 adapted ZF,FOL,CCL,LCF to modified splitter
2015-07-28 wenzelm 2015-07-28 more explicit context;
2015-04-08 wenzelm 2015-04-08 proper context for Object_Logic operations;
2015-03-07 wenzelm 2015-03-07 clarified Drule.gen_all: observe context more carefully;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-01-12 wenzelm 2014-01-12 tuned signature; clarified context;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2011-11-28 wenzelm 2011-11-28 avoid stepping outside of context -- plain zero_var_indexes should be sufficient;
2011-11-24 wenzelm 2011-11-24 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-23 wenzelm 2011-11-23 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-06-29 wenzelm 2011-06-29 tuned signature;
2011-06-29 wenzelm 2011-06-29 simplified/unified Simplifier.mk_solver;
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-04-26 wenzelm 2011-04-26 modernized Clasimp setup;
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