src/HOL/Tools/inductive_package.ML
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).
1999-06-28 wenzelm 1999-06-28 cond_extern_table;
1999-05-25 wenzelm 1999-05-25 formal comments (still dummy);
1999-05-24 wenzelm 1999-05-24 outer syntax keyword classification; no open OuterParse;
1999-04-30 wenzelm 1999-04-30 theory data: copy;
1999-04-27 wenzelm 1999-04-27 intrs attributes;
1999-04-16 wenzelm 1999-04-16 'HOL/inductive' theory data;
1999-04-14 wenzelm 1999-04-14 triple_swap;
1999-04-14 wenzelm 1999-04-14 tuned messages;
1999-04-14 wenzelm 1999-04-14 tuned comments; intrs: names and atts; Isar outer syntax;
1999-03-17 wenzelm 1999-03-17 Theory.sign_of;
1999-01-19 paulson 1999-01-19 removal of the (thm list) argument of mk_cases
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-11-16 wenzelm 1998-11-16 Attribute.tthms_of;
1998-10-21 berghofe 1998-10-21 Changed interface of add_inductive: monos and con_defs are now lists of xstrings.
1998-10-16 berghofe 1998-10-16 Added quiet_mode flag.
1998-09-24 oheimb 1998-09-24 renamed mk_meta_eq to mk_eq
1998-08-12 oheimb 1998-08-12 renamed mk_meta_eq to meta_eq
1998-07-24 berghofe 1998-07-24 Replaced Nat.thy by NatDef.thy because Nat.thy depends on inductive_package.
1998-07-15 berghofe 1998-07-15 Fixed bug in transform_rule.
1998-07-03 berghofe 1998-07-03 Removed disjE from list of rules used to simplify elimination rules because it made mk_cases fail if elimination rules contained disjunctive side conditions.
1998-07-01 berghofe 1998-07-01 Fixed bug (improper handling of flag no_ind).
1998-06-30 berghofe 1998-06-30 New inductive definition package