src/HOL/Tools/Function/induction_schema.ML
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-06 wenzelm 2015-03-06 clarified 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
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-03-07 blanchet 2014-03-07 tuning
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
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-06-27 wenzelm 2013-06-27 tuned signature;
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-04-12 wenzelm 2012-04-12 more standard method setup;
2012-02-14 wenzelm 2012-02-14 comment;
2012-01-14 wenzelm 2012-01-14 renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
2011-04-27 wenzelm 2011-04-27 clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-12-29 krauss 2010-12-29 more robust decomposition of simultaneous goals
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-12-17 wenzelm 2010-12-17 refer to regular structure Simplifier;
2010-12-13 krauss 2010-12-13 eliminated dest_all_all_ctx
2010-09-28 krauss 2010-09-28 consolidated tupled_lambda; moved to structure HOLogic
2010-07-01 haftmann 2010-07-01 qualified constants Set.member and Set.Collect
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-01-02 krauss 2010-01-02 new year's resolution: reindented code in function package
2009-11-23 krauss 2009-11-23 eliminated dead code and some unused bindings, reported by polyml
2009-11-15 wenzelm 2009-11-15 tuned;
2009-11-06 krauss 2009-11-06 renamed method induct_scheme to induction_schema