src/ZF/Epsilon.thy

--- a/src/ZF/Epsilon.thy	Thu Jan 07 11:08:29 1999 +0100
+++ b/src/ZF/Epsilon.thy	Thu Jan 07 18:30:55 1999 +0100
@@ -25,4 +25,10 @@
                            b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
                            UN j<i. r`j)))"
 
+    recursor  :: [i, [i,i]=>i, i]=>i
+     "recursor(a,b,k) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
+
+    rec  :: [i, i, [i,i]=>i]=>i
+     "rec(k,a,b) ==  recursor(a,b,k)"
+
 end