src/HOL/Tools/inductive_package.ML
2001-12-29 ago 'inductive_cases': support 'and' form;
2001-12-18 ago tuned Type.unify;
2001-12-14 ago changed Type.varify;
2001-12-06 ago added the_mk_cases;
2001-12-01 ago renamed class "term" to "type" (actually "HOL.type");
2001-11-28 ago theory data: removed obsolete finish method;
2001-11-21 ago Set.vimage;
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;