src/ZF/Main.thy

--- a/src/ZF/Main.thy	Wed Jan 02 21:54:45 2002 +0100
+++ b/src/ZF/Main.thy	Thu Jan 03 17:01:59 2002 +0100
@@ -46,4 +46,14 @@
 lemmas posDivAlg_induct = posDivAlg_induct [consumes 2]
   and negDivAlg_induct = negDivAlg_induct [consumes 2]
 
+
+(* belongs to theory Epsilon *)
+
+lemma def_transrec2:
+     "(!!x. f(x)==transrec2(x,a,b))
+      ==> f(0) = a & 
+          f(succ(i)) = b(i, f(i)) & 
+          (Limit(K) --> f(K) = (UN j<K. f(j)))"
+by (simp add: transrec2_Limit)
+
 end