diff -r 4d1614d8f119 -r 70b789956bd3 src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Thu Jul 21 16:51:26 1994 +0200
+++ b/src/ZF/CardinalArith.thy	Tue Jul 26 13:21:20 1994 +0200
@@ -6,22 +6,18 @@
 Cardinal Arithmetic
 *)
 
-CardinalArith = Cardinal + OrderArith + Arith + 
+CardinalArith = Cardinal + OrderArith + Arith + Fin + 
 consts
-  jump_cardinal :: "i=>i"
 
   InfCard     :: "i=>o"
   "|*|"       :: "[i,i]=>i"       (infixl 70)
   "|+|"       :: "[i,i]=>i"       (infixl 65)
   csquare_rel :: "i=>i"
+  jump_cardinal :: "i=>i"
+  csucc       :: "i=>i"
 
 rules
 
-  jump_cardinal_def
-      "jump_cardinal(K) ==   \
-\         UN X:Pow(K). {z. r: Pow(X*X), well_ord(X,r) & z = ordertype(X,r)}"
-
-
   InfCard_def  "InfCard(i) == Card(i) & nat le i"
 
   cadd_def     "i |+| j == | i+j |"
@@ -33,4 +29,13 @@
 \                            rmult(k,Memrel(k), k*k, 	\
 \                                  rmult(k,Memrel(k), k,Memrel(k))))"
 
+  (*This def is more complex than Kunen's but it more easily proved to
+    be a cardinal*)
+  jump_cardinal_def
+      "jump_cardinal(K) ==   \
+\         UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"
+
+  (*needed because jump_cardinal(K) might not be the successor of K*)
+  csucc_def "csucc(K) == LEAST L. Card(L) & K<L"
+
 end