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