src/HOL/Tools/inductive_package.ML
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