src/HOL/Tools/inductive_package.ML
2001-10-15 wenzelm 2001-10-15 Tactic.rewrite_cterm;
2001-10-14 wenzelm 2001-10-14 moved rulify to ObjectLogic;
2001-10-14 wenzelm 2001-10-14 "HOL.mono";
2001-10-13 wenzelm 2001-10-13 IsarThy.theorem_i Drule.internalK;
2001-10-04 wenzelm 2001-10-04 simp_case_tac is back again from induct_method.ML; tuned;
2001-09-28 wenzelm 2001-09-28 inductive: no collective atts;
2001-08-16 wenzelm 2001-08-16 prefer immediate monos; tuned;
2001-06-01 paulson 2001-06-01 now checks for leading meta-quantifiers and complains, instead of just raising an exception
2001-02-02 wenzelm 2001-02-02 use hol_simplify;
2001-01-31 wenzelm 2001-01-31 more robust handling of rule cases hints;
2001-01-29 berghofe 2001-01-29 Splitting of arguments of product types in induction rules is now less aggressive.
2001-01-16 wenzelm 2001-01-16 export inductive_forall_name, inductive_forall_def, rulify;
2001-01-06 wenzelm 2001-01-06 Tactic.norm_hhf;
2000-12-27 wenzelm 2000-12-27 Method.erule 0;
2000-12-23 wenzelm 2000-12-23 simplified quick_and_dirty stuff; tuned;
2000-12-22 wenzelm 2000-12-22 handle proper rules;
2000-12-01 wenzelm 2000-12-01 ignore quick_and_dirty for coind;
2000-10-19 wenzelm 2000-10-19 InductAttrib;
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-10-12 nipkow 2000-10-12 induct -> lfp_induct
2000-10-11 nipkow 2000-10-11 *** empty log message ***
2000-09-23 paulson 2000-09-23 renaming the inverse image operator in HOL
2000-09-17 wenzelm 2000-09-17 Display.pretty_thm_sg;
2000-09-12 wenzelm 2000-09-12 tuned handling of "intros";
2000-09-07 wenzelm 2000-09-07 tuned msg;
2000-09-04 wenzelm 2000-09-04 tuned "mono" att setup;
2000-09-02 wenzelm 2000-09-02 "inductive_cases": proper command;
2000-08-17 wenzelm 2000-08-17 removed obsolete keyword;
2000-08-17 wenzelm 2000-08-17 renamed 'mk_cases_tac' to 'ind_cases';
2000-08-14 wenzelm 2000-08-14 raplaced "intrs" by "intrs" (new-style only); improved new-style interface to mk_cases;
2000-08-09 wenzelm 2000-08-09 fixed mk_cases_i: TRYALL InductMethod.simp_case_tac;
2000-07-22 wenzelm 2000-07-22 improved error msg; thm foo.cases;
2000-07-13 wenzelm 2000-07-13 adapted PureThy.add_defs_i;
2000-07-13 wenzelm 2000-07-13 use InductMethod.simp_case_tac;
2000-07-03 wenzelm 2000-07-03 previde 'defs' field for quick_and_dirty;
2000-06-29 wenzelm 2000-06-29 adapted args of IsarThy.have_theorems_i;
2000-06-23 berghofe 2000-06-23 get_inductive now returns None instead of raising an exception.
2000-06-15 berghofe 2000-06-15 Now also proves monotonicity when in quick_and_dirty mode.
2000-04-17 wenzelm 2000-04-17 Pretty.chunks;
2000-03-31 wenzelm 2000-03-31 use Attrib.add_del_args;
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.; tuned case names;
2000-03-10 berghofe 2000-03-10 Type.unify now uses Vartab instead of association lists.
2000-03-09 wenzelm 2000-03-09 more robust case names of induct;
2000-03-08 wenzelm 2000-03-08 removed tune_names;
2000-03-08 wenzelm 2000-03-08 mk_elims, add_cases_induct: name rule cases;
2000-03-03 wenzelm 2000-03-03 mk_cases / inductive_cases: use InductMethod.con_elim_(solved_)tac;
2000-02-29 wenzelm 2000-02-29 add_cases_induct: project_rules accomodates mutual induction;
2000-02-28 wenzelm 2000-02-28 add_cases_induct: accomodate no_elim and no_ind flags;
2000-02-27 wenzelm 2000-02-27 add_cases_induct: induct_method setup; removed cases_of, all_cases, all_inducts;
2000-02-24 wenzelm 2000-02-24 all_cases / all_inducts;
2000-02-22 wenzelm 2000-02-22 added cases_of, cases;
2000-01-05 wenzelm 2000-01-05 replaced HOLogic.termTVar by HOLogic.termT;
1999-10-08 wenzelm 1999-10-08 return stored thms with proper naming in derivation;
1999-10-05 berghofe 1999-10-05 Monotonicity rules for inductive definitions can now be added to a theory via attribute "mono".
1999-08-25 berghofe 1999-08-25 Removed "Adding axioms ..." message.
1999-08-19 berghofe 1999-08-19 Moved sum_case stuff from Sum to Datatype.
1999-08-18 berghofe 1999-08-18 Renamed sum_case to basic_sum_case.
1999-08-02 wenzelm 1999-08-02 tuned outer syntax;
1999-07-27 wenzelm 1999-07-27 inductive_cases(_i): Isar interface to mk_cases;
1999-07-16 berghofe 1999-07-16 Exported function unify_consts (workaround to avoid inconsistently typed recursive constants in inductive and primrec definitions).