src/ZF/Univ.thy
changeset 1155 928a16e02f9f
parent 796 357a1f2dd07e
child 1401 0c439768f45c
--- a/src/ZF/Univ.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Univ.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -25,8 +25,8 @@
     Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
 
     Vrec_def
-   	"Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).      \
-\                             H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
+   	"Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).      
+                             H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
 
     univ_def    "univ(A) == Vfrom(A,nat)"