2001-11-14 ago inductive: removed con_defs;
2001-11-13 ago tuned;
2001-11-12 ago mutual rules declared as ``consumes 0'';
2001-11-09 ago tuned;
2001-11-08 ago theory data: finish method;
2001-10-31 ago use HOL.induct_XXX;
2001-10-22 ago quick_and_dirty_prove_goalw_cterm;
2001-10-18 ago GPLed;
2001-10-18 ago moved atomize stuff to theory HOL;
2001-10-15 ago Tactic.rewrite_cterm;
2001-10-14 ago moved rulify to ObjectLogic;
2001-10-14 ago "HOL.mono";
2001-10-13 ago IsarThy.theorem_i Drule.internalK;
2001-10-04 ago simp_case_tac is back again from induct_method.ML;
2001-09-28 ago inductive: no collective atts;
2001-08-16 ago prefer immediate monos;
2001-06-01 ago now checks for leading meta-quantifiers and complains, instead of
2001-02-02 ago use hol_simplify;
2001-01-31 ago more robust handling of rule cases hints;
2001-01-29 ago Splitting of arguments of product types in induction rules is now less
2001-01-16 ago export inductive_forall_name, inductive_forall_def, rulify;
2001-01-06 ago Tactic.norm_hhf;
2000-12-27 ago Method.erule 0;
2000-12-23 ago simplified quick_and_dirty stuff;
2000-12-22 ago handle proper rules;
2000-12-01 ago ignore quick_and_dirty for coind;
2000-10-19 ago InductAttrib;
2000-10-12 ago *** empty log message ***
2000-10-12 ago induct -> lfp_induct
2000-10-11 ago *** empty log message ***
2000-09-23 ago renaming the inverse image operator in HOL
2000-09-17 ago Display.pretty_thm_sg;
2000-09-12 ago tuned handling of "intros";
2000-09-07 ago tuned msg;
2000-09-04 ago tuned "mono" att setup;
2000-09-02 ago "inductive_cases": proper command;
2000-08-17 ago removed obsolete keyword;
2000-08-17 ago renamed 'mk_cases_tac' to 'ind_cases';
2000-08-14 ago raplaced "intrs" by "intrs" (new-style only);
2000-08-09 ago fixed mk_cases_i: TRYALL InductMethod.simp_case_tac;
2000-07-22 ago improved error msg;
2000-07-13 ago adapted PureThy.add_defs_i;
2000-07-13 ago use InductMethod.simp_case_tac;
2000-07-03 ago previde 'defs' field for quick_and_dirty;
2000-06-29 ago adapted args of IsarThy.have_theorems_i;
2000-06-23 ago get_inductive now returns None instead of raising an exception.
2000-06-15 ago Now also proves monotonicity when in quick_and_dirty mode.
2000-04-17 ago Pretty.chunks;
2000-03-31 ago use Attrib.add_del_args;
2000-03-13 ago adapted to new PureThy.add_thms etc.;
2000-03-10 ago Type.unify now uses Vartab instead of association lists.
2000-03-09 ago more robust case names of induct;
2000-03-08 ago removed tune_names;
2000-03-08 ago mk_elims, add_cases_induct: name rule cases;
2000-03-03 ago mk_cases / inductive_cases: use InductMethod.con_elim_(solved_)tac;
2000-02-29 ago add_cases_induct: project_rules accomodates mutual induction;
2000-02-28 ago add_cases_induct: accomodate no_elim and no_ind flags;
2000-02-27 ago add_cases_induct: induct_method setup;
2000-02-24 ago all_cases / all_inducts;
2000-02-22 ago added cases_of, cases;