src/ZF/Univ.thy

--- a/src/ZF/Univ.thy	Mon Dec 28 16:58:11 1998 +0100
+++ b/src/ZF/Univ.thy	Mon Dec 28 16:59:28 1998 +0100
@@ -19,6 +19,7 @@
     Vfrom       :: [i,i]=>i
     Vset        :: i=>i
     Vrec        :: [i, [i,i]=>i] =>i
+    Vrecursor   :: [[i,i]=>i, i] =>i
     univ        :: i=>i
 
 translations
@@ -33,6 +34,10 @@
         "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).      
                              H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
 
+    Vrecursor_def
+        "Vrecursor(H,a) == transrec(rank(a), %x g. lam z: Vset(succ(x)).      
+                                    H(lam w:Vset(x). g`rank(w)`w, z)) ` a"
+
     univ_def    "univ(A) == Vfrom(A,nat)"
 
 end