--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/Transrec2.thy Fri Mar 31 11:55:29 1995 +0200
@@ -0,0 +1,23 @@
+(* Title: ZF/AC/Transrec2.thy
+ ID: $Id$
+ Author: Krzysztof Gr`abczewski
+
+Transfinite recursion introduced to handle definitions based on the three
+cases of ordinals.
+*)
+
+Transrec2 = OrdQuant + Epsilon +
+
+consts
+
+ transrec2 :: "[i, i, [i,i]=>i] =>i"
+
+defs
+
+ transrec2_def "transrec2(alpha, a, b) == \
+\ transrec(alpha, %i r. if(i=0, \
+\ a, if(EX j. i=succ(j), \
+\ b(THE j. i=succ(j), r`(THE j. i=succ(j))), \
+\ UN j<i. r`j)))"
+
+end