src/HOL/Tools/induct_method.ML
2000-07-01 wenzelm 2000-07-01 GPLed;
2000-06-14 wenzelm 2000-06-14 theorems [cases type: bool] = case_split;
2000-05-05 wenzelm 2000-05-05 use Args.colon / Args.parens;
2000-04-12 wenzelm 2000-04-12 export concl_of; induct method: admit "_";
2000-04-12 wenzelm 2000-04-12 induct stripped: match_tac;
2000-04-05 wenzelm 2000-04-05 HEADGOAL;
2000-03-20 wenzelm 2000-03-20 tuned degenerate cases / induct;
2000-03-14 wenzelm 2000-03-14 tuned comments;
2000-03-13 wenzelm 2000-03-13 export vars_of;
2000-03-09 wenzelm 2000-03-09 cleaned comment;
2000-03-08 wenzelm 2000-03-08 added dest_global/local_rules; cases/induct: tuned rule selection, always admit insts; accomodate rule case names;
2000-03-04 wenzelm 2000-03-04 induct: "stripped" option;
2000-03-03 wenzelm 2000-03-03 added con_elim_s(olved_)tac; added 'simplified' flag;
2000-03-03 wenzelm 2000-03-03 join_rules: compatibility check;
2000-03-02 wenzelm 2000-03-02 join induct rules;
2000-02-29 wenzelm 2000-02-29 tuned msgs;
2000-02-27 wenzelm 2000-02-27 cases/induct attributes; use NetRules for storage; tuned rule selection; tuned concrete syntax;
2000-02-24 wenzelm 2000-02-24 induct method: implicit rule;
2000-02-22 wenzelm 2000-02-22 induct: tuned syntax; added cases method;
2000-01-28 wenzelm 2000-01-28 replaced FIRSTGOAL by FINDGOAL (backtracking!);
1999-09-07 wenzelm 1999-09-07 rule option;
1999-07-16 berghofe 1999-07-16 Replaced datatype_info by datatype_info_err.
1999-04-27 wenzelm 1999-04-27 support forward chaining;
1999-04-16 wenzelm 1999-04-16 may specify induction predicates as well;
1999-04-16 wenzelm 1999-04-16 Proof by induction on types / set / functions.