src/HOL/Tools/inductive_package.ML
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;
2000-01-05 ago replaced HOLogic.termTVar by HOLogic.termT;
1999-10-08 ago return stored thms with proper naming in derivation;
1999-10-05 ago Monotonicity rules for inductive definitions can now be added to a theory via
1999-08-25 ago Removed "Adding axioms ..." message.
1999-08-19 ago Moved sum_case stuff from Sum to Datatype.
1999-08-18 ago Renamed sum_case to basic_sum_case.
1999-08-02 ago tuned outer syntax;
1999-07-27 ago inductive_cases(_i): Isar interface to mk_cases;
1999-07-16 ago Exported function unify_consts (workaround to avoid inconsistently
1999-06-28 ago cond_extern_table;
1999-05-25 ago formal comments (still dummy);
1999-05-24 ago outer syntax keyword classification;
1999-04-30 ago theory data: copy;
1999-04-27 ago intrs attributes;
1999-04-16 ago 'HOL/inductive' theory data;
1999-04-14 ago triple_swap;
1999-04-14 ago tuned messages;
1999-04-14 ago tuned comments;
1999-03-17 ago Theory.sign_of;
1999-01-19 ago removal of the (thm list) argument of mk_cases
1999-01-12 ago eliminated tthm type and Attribute structure;
1998-11-16 ago Attribute.tthms_of;