--- a/src/ZF/upair.ML Fri Sep 24 11:27:15 1993 +0200
+++ b/src/ZF/upair.ML Thu Sep 30 10:10:21 1993 +0100
@@ -235,17 +235,21 @@
"i : j ==> i : succ(j)"
(fn [prem]=> [ (rtac (prem RS consI2) 1) ]);
-(*Classical introduction rule*)
-val succCI = prove_goalw ZF.thy [succ_def]
- "(~ i:j ==> i=j) ==> i: succ(j)"
- (fn prems=> [ (rtac consCI 1), (eresolve_tac prems 1) ]);
-
val succE = prove_goalw ZF.thy [succ_def]
"[| i : succ(j); i=j ==> P; i:j ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS consE) 1),
(REPEAT (eresolve_tac prems 1)) ]);
+val succ_iff = prove_goal ZF.thy "i : succ(j) <-> i=j | i:j"
+ (fn _ => [ (fast_tac (lemmas_cs addIs [succI1,succI2] addSEs [succE]) 1) ]);
+
+(*Classical introduction rule*)
+val succCI = prove_goal ZF.thy "(~ i:j ==> i=j) ==> i: succ(j)"
+ (fn [prem]=>
+ [ (rtac (disjCI RS (succ_iff RS iffD2)) 1),
+ (etac prem 1) ]);
+
val succ_neq_0 = prove_goal ZF.thy "succ(n)=0 ==> P"
(fn [major]=>
[ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1),