src/Tools/induct_tacs.ML
21 months ago wenzelm 2017-12-06 prefer control symbol antiquotations;
2016-05-23 wenzelm 2016-05-23 embedded content may be delimited via cartouches;
2015-07-08 wenzelm 2015-07-08 Variable.focus etc.: optional bindings provided by user; Subgoal.focus command: more careful treatment of user-provided bindings;
2015-03-28 wenzelm 2015-03-28 clarified goal context;
2015-03-28 wenzelm 2015-03-28 clarified goal context;
2015-03-27 wenzelm 2015-03-27 proper Rule_Insts.read_term, e.g. to enable case_tac using "_";
2015-03-27 wenzelm 2015-03-27 tuned signature;
2015-03-24 wenzelm 2015-03-24 clarified case_tac fixes and context;
2015-03-24 wenzelm 2015-03-24 clarified input source;
2015-03-23 wenzelm 2015-03-23 support 'for' fixes in rule_tac etc.;
2015-03-20 wenzelm 2015-03-20 tuned signature;
2015-03-19 wenzelm 2015-03-19 more position information;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-02-24 wenzelm 2014-02-24 tuned messages -- prefer quote before Position.here, which might be just \<here>;
2014-01-22 wenzelm 2014-01-22 tuned signature;
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-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2012-03-09 wenzelm 2012-03-09 tuned signature;
2012-03-08 wenzelm 2012-03-08 more precise warning/error positions;
2011-10-12 wenzelm 2011-10-12 modernized structure Induct_Tacs;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
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;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-01 wenzelm 2009-11-01 modernized structure Rule_Cases;
2009-10-02 wenzelm 2009-10-02 eliminated dead code; tuned;
2009-03-15 wenzelm 2009-03-15 simplified method setup;
2009-02-28 wenzelm 2009-02-28 removed Ids;
2008-09-22 haftmann 2008-09-22 fixed headers
2008-08-15 wenzelm 2008-08-15 Args.name_source(_position) for proper position information;
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;
2008-06-23 wenzelm 2008-06-23 induct_tac: allow omission of arguments;
2008-06-23 wenzelm 2008-06-23 moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;