src/ZF/CardinalArith.thy

--- a/src/ZF/CardinalArith.thy	Sun Apr 24 21:31:14 2016 +0200
+++ b/src/ZF/CardinalArith.thy	Mon Apr 25 16:09:26 2016 +0200
@@ -28,7 +28,7 @@
 
 definition
   jump_cardinal :: "i=>i"  where
-    \<comment>\<open>This def is more complex than Kunen's but it more easily proved to
+    \<comment>\<open>This definition is more complex than Kunen's but it more easily proved to
         be a cardinal\<close>
     "jump_cardinal(K) ==
          \<Union>X\<in>Pow(K). {z. r \<in> Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}"