src/Tools/eqsubst.ML
17 months ago wenzelm 2017-12-06 prefer control symbol antiquotations;
2015-06-02 wenzelm 2015-06-02 clarified context;
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
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-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-09-11 blanchet 2014-09-11 fixed some spelling mistakes
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-08-23 wenzelm 2013-08-23 tuned signature;
2013-07-27 wenzelm 2013-07-27 standardized aliases;
2013-05-30 wenzelm 2013-05-30 tuned signature;
2013-05-30 wenzelm 2013-05-30 more standard fold/fold_rev;
2013-05-30 wenzelm 2013-05-30 misc tuning;
2013-05-30 wenzelm 2013-05-30 prefer existing beta_eta_conversion;
2013-05-30 wenzelm 2013-05-30 more standard names;
2013-05-30 wenzelm 2013-05-30 simplified method setup;
2013-05-30 wenzelm 2013-05-30 tuned -- prefer terminology of tactic / goal state;
2013-05-30 wenzelm 2013-05-30 tuned;
2013-05-30 wenzelm 2013-05-30 misc tuning;
2013-05-29 wenzelm 2013-05-29 tuned signature -- more explicit flags for low-level Thm.bicompose;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-09-12 wenzelm 2012-09-12 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
2012-09-12 wenzelm 2012-09-12 eliminated some old material that is unused in the visible universe;
2011-08-09 wenzelm 2011-08-09 misc tuning and simplification;
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2010-12-15 wenzelm 2010-12-15 avoid ML structure aliases (especially single-letter abbreviations);
2010-11-26 wenzelm 2010-11-26 make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2009-10-27 wenzelm 2009-10-27 normalized basic type abbreviations;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
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-17 wenzelm 2009-07-17 tuned/modernized Envir operations;
2009-05-30 wenzelm 2009-05-30 minimal signature cleanup; modernized method setup;
2009-03-13 wenzelm 2009-03-13 eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-06 wenzelm 2009-03-06 replaced archaic use of rep_ss by Simplifier.mksimps;
2009-02-28 wenzelm 2009-02-28 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;