--- a/src/ZF/Cardinal.ML Thu Apr 13 10:20:55 1995 +0200
+++ b/src/ZF/Cardinal.ML Thu Apr 13 11:30:57 1995 +0200
@@ -188,7 +188,7 @@
by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
qed "less_LeastE";
-(*Easier to apply than LeastI2: conclusion has only one occurrence of P*)
+(*Easier to apply than LeastI: conclusion has only one occurrence of P*)
qed_goal "LeastI2" Cardinal.thy
"[| P(i); Ord(i); !!j. P(j) ==> Q(j) |] ==> Q(LEAST j. P(j))"
(fn prems => [ resolve_tac prems 1,
@@ -440,6 +440,11 @@
by (fast_tac (ZF_cs addSIs [inj_not_surj_succ]) 1);
qed "lesspoll_succ_imp_lepoll";
+goal Cardinal.thy "!!m. m:nat ==> A lesspoll succ(m) <-> A lepoll m";
+by (fast_tac (ZF_cs addSIs [lepoll_imp_lesspoll_succ,
+ lesspoll_succ_imp_lepoll]) 1);
+qed "lesspoll_succ_iff";
+
goal Cardinal.thy "!!A m. [| A lepoll succ(m); m:nat |] ==> \
\ A lepoll m | A eqpoll succ(m)";
by (rtac disjCI 1);