src/HOL/Tools/simpdata.ML
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-03-13 nipkow 2014-03-13 enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
2014-01-12 wenzelm 2014-01-12 tuned signature; clarified context;
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
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 tuned;
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;
2011-04-16 wenzelm 2011-04-16 eliminated old List.nth; tuned;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
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-19 haftmann 2010-08-19 tuned quotes
2010-07-08 haftmann 2010-07-08 tuned titles
2010-04-30 wenzelm 2010-04-30 renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
2010-04-29 wenzelm 2010-04-29 proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-02-25 wenzelm 2010-02-25 more antiquotations;
2010-02-19 wenzelm 2010-02-19 renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
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-03-20 wenzelm 2009-03-20 Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s