src/ZF/Zorn.thy
changeset 1155 928a16e02f9f
parent 806 6330ca0a3ac5
child 1401 0c439768f45c
--- a/src/ZF/Zorn.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Zorn.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -39,8 +39,8 @@
 inductive
   domains       "TFin(S,next)" <= "Pow(S)"
   intrs
-    nextI	"[| x : TFin(S,next);  next: increasing(S) \
-\                |] ==> next`x : TFin(S,next)"
+    nextI	"[| x : TFin(S,next);  next: increasing(S) 
+                |] ==> next`x : TFin(S,next)"
 
     Pow_UnionI	"Y : Pow(TFin(S,next)) ==> Union(Y) : TFin(S,next)"