| changeset 770 | 216ec1299bf0 |
| parent 760 | f0200e91b272 |
| child 782 | 200a16083201 |
--- a/src/ZF/OrderArith.ML Thu Dec 08 14:38:58 1994 +0100 +++ b/src/ZF/OrderArith.ML Thu Dec 08 15:07:48 1994 +0100 @@ -62,9 +62,6 @@ (** Linearity **) -val sum_ss = ZF_ss addsimps [Pair_iff, InlI, InrI, Inl_iff, Inr_iff, - Inl_Inr_iff, Inr_Inl_iff]; - val radd_ss = sum_ss addsimps [radd_Inl_iff, radd_Inr_iff, radd_Inl_Inr_iff, radd_Inr_Inl_iff];