src/Tools/coherent.ML
15 months ago wenzelm 2018-01-28 clarified take/drop/chop prefix/suffix;
17 months ago wenzelm 2017-12-06 prefer control symbol antiquotations;
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
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-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-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-02-20 wenzelm 2014-02-20 more official params in context;
2014-02-20 wenzelm 2014-02-20 tuned messages; more official hyps;
2014-02-20 wenzelm 2014-02-20 modernized tool setup; tuned;
2014-02-20 wenzelm 2014-02-20 removed dead code;
2014-02-20 wenzelm 2014-02-20 prefer cat_lines;
2014-02-20 wenzelm 2014-02-20 tuned whitespace;
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
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;
2012-01-11 wenzelm 2012-01-11 more qualified names; more antiquotations;
2011-04-27 wenzelm 2011-04-27 reorganized fixes as specialized (global) name space;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-05-15 wenzelm 2010-05-15 avoid open Conv;
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-28 wenzelm 2009-09-28 misc tuning and modernization;
2009-07-26 wenzelm 2009-07-26 Variable.focus: named parameters;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir.subst_XXX;
2009-06-29 berghofe 2009-06-29 Corrected handling of bound variables.
2009-05-25 wenzelm 2009-05-25 modernized method setup; tuned signature;
2009-03-16 wenzelm 2009-03-16 provide Simplifier.norm_hhf(_protect) as regular simplifier operation;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-02-28 wenzelm 2009-02-28 tuned message;
2009-02-28 wenzelm 2009-02-28 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;