src/Tools/induction.ML
17 months ago wenzelm 2017-12-06 prefer control symbol antiquotations;
2015-12-14 wenzelm 2015-12-14 tuned signature;
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-04-08 wenzelm 2015-04-08 proper context for Object_Logic operations;
2015-04-06 wenzelm 2015-04-06 local setup of induction tools, with restricted access to auxiliary consts; proper antiquotations for formerly inaccessible consts;
2015-04-06 wenzelm 2015-04-06 proper header; misc tuning;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-04-10 wenzelm 2014-04-10 tuned;
2011-09-20 nipkow 2011-09-20 New proof method "induction" that gives induction hypotheses the name IH.