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)"