| changeset 1985 | 84cf16192e03 |
| parent 1867 | 37615e73f2d8 |
| child 2031 | 03a843f0f447 |
--- a/src/HOL/indrule.ML Thu Sep 12 10:36:51 1996 +0200 +++ b/src/HOL/indrule.ML Thu Sep 12 10:40:05 1996 +0200 @@ -165,7 +165,7 @@ (*Simplification largely reduces the mutual induction rule to the standard rule*) -val mut_ss = min_ss addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq, split]; +val mut_ss = min_ss addsimps [Inl_not_Inr, Inr_not_Inl, Inl_eq, Inr_eq, split]; val all_defs = [split RS eq_reflection] @ Inductive.con_defs @ part_rec_defs;