src/FOL/simpdata.ML
2021-09-19 wenzelm clarified signature -- prefer antiquotations (with subtle change of exception content);
2021-09-11 wenzelm more antiquotations;
2020-05-30 haftmann specific atomization inert to later rule set modifications
2019-01-04 wenzelm isabelle update -u control_cartouches;
2016-08-09 nipkow adapted ZF,FOL,CCL,LCF to modified splitter
2015-07-28 wenzelm more explicit context;
2015-04-08 wenzelm proper context for Object_Logic operations;
2015-03-07 wenzelm clarified Drule.gen_all: observe context more carefully;
2015-03-04 wenzelm tuned signature -- prefer qualified names;
2015-02-10 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
2014-11-10 wenzelm proper context for assume_tac (atac remains as fall-back without context);
2014-11-09 wenzelm proper context for match_tac etc.;
2014-10-30 wenzelm eliminated aliases;
2014-03-21 wenzelm more qualified names;
2014-01-12 wenzelm tuned signature;
2013-04-18 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
2011-11-28 wenzelm avoid stepping outside of context -- plain zero_var_indexes should be sufficient;
2011-11-24 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-23 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-06-29 wenzelm tuned signature;
2011-06-29 wenzelm simplified/unified Simplifier.mk_solver;
2011-05-13 wenzelm proper Proof.context for classical tactics;
2011-04-26 wenzelm modernized Clasimp setup;
2011-04-22 wenzelm simplified Data signature;
2011-04-22 wenzelm misc tuning;
2011-04-22 wenzelm modernized Quantifier1 simproc setup;
2011-04-22 wenzelm clarified simpset setup;
2010-12-20 wenzelm proper identifiers for consts and types;
2010-08-25 wenzelm renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-08-17 haftmann more antiquotations
2010-04-30 wenzelm removed some old comments;
2010-04-30 wenzelm proper context for rule_by_tactic;
2010-04-29 wenzelm proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-02-19 wenzelm renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2010-02-07 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-10-16 wenzelm explicitly qualify Drule.standard;
2009-10-15 wenzelm replaced String.concat by implode;
2009-07-24 wenzelm renamed functor SplitterFun to Splitter, require explicit theory;
2009-07-23 wenzelm more @{theory} antiquotations;
2009-07-23 wenzelm renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-15 wenzelm more antiquotations;
2009-07-09 wenzelm removed obsolete CVS Ids;
2009-03-20 wenzelm Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
2008-09-17 wenzelm back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-06-24 wenzelm ML_Antiquote.value;
2008-03-29 wenzelm purely functional setup of claset/simpset/clasimpset;
2008-03-15 wenzelm eliminated out-of-scope proofs (cf. theory IFOL and FOL);
2007-04-27 wenzelm removed obsolete induct/simp tactic;
2007-01-20 wenzelm added @{clasimpset};
2006-11-26 wenzelm converted legacy ML scripts;
2006-07-27 wenzelm tuned proofs;
2006-01-19 wenzelm setup: theory -> theory;
2005-12-31 wenzelm removed obsolete Provers/make_elim.ML;
2005-12-01 wenzelm unfold_tac: static evaluation of simpset;
2005-10-18 wenzelm Simplifier.theory_context;
2005-10-17 wenzelm change_claset/simpset;
2005-09-12 haftmann introduced new-style AList operations
2005-08-02 wenzelm simprocs: Simplifier.inherit_bounds;
2005-05-22 wenzelm Simplifier already setup in Pure;
2005-03-03 skalberg Move towards standard functions.
less more (0) -100 -60 tip