src/HOL/Tools/TFL/post.ML
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-03-03 traytel 2015-03-03 eliminated some clones of Proof_Context.cterm_of
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-03-21 wenzelm 2014-03-21 more qualified names;
2014-02-01 wenzelm 2014-02-01 proper context for printing;
2014-01-26 wenzelm 2014-01-26 tuned signature;
2014-01-25 wenzelm 2014-01-25 explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
2014-01-12 wenzelm 2014-01-12 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;
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);
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-05-12 wenzelm 2011-05-12 prefer Proof.context over old-style claset/simpset; canonical argument order;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-04 krauss 2011-03-04 clarified
2010-12-15 wenzelm 2010-12-15 avoid ML structure aliases (especially single-letter abbreviations);
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-05-03 wenzelm 2010-05-03 replaced Thm.legacy_freezeT by Thm.unvarify_global -- these facts stem from closed definitions, i.e. there are no term Vars;
2010-05-03 wenzelm 2010-05-03 renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-30 wenzelm 2010-04-30 proper context for rule_by_tactic;
2010-03-15 wenzelm 2010-03-15 preserve full const name more carefully, and avoid slightly odd Sign.intern_term;
2010-03-12 bulwahn 2010-03-12 refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-25 wenzelm 2010-02-25 modernized structure Split_Rule; tuned signature; more antiquotations;
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-11-21 wenzelm 2009-11-21 explicitly mark some legacy freeze operations;
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-27 wenzelm 2009-10-27 eliminated some old folds;
2009-10-21 haftmann 2009-10-21 curried union as canonical list operation
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-17 wenzelm 2009-10-17 removed obsolete old goal command;
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-03-27 haftmann 2009-03-27 dropped legacy goal package call
2009-03-23 haftmann 2009-03-23 moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2008-12-10 wenzelm 2008-12-10 more antiquotations;
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-16 wenzelm 2008-06-16 RuleInsts.read_instantiate;
2008-06-11 wenzelm 2008-06-11 Drule.read_instantiate;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-29 wenzelm 2008-03-29 eliminated quiete_mode ref (not really needed);
2007-09-25 wenzelm 2007-09-25 Syntax.parse/check/read;
2007-07-31 wenzelm 2007-07-31 arith method setup: proper context;
2007-07-20 haftmann 2007-07-20 dropped Nat.ML legacy bindings
2007-05-31 wenzelm 2007-05-31 moved TFL files to canonical place;