changeset 12620 | 4e6626725e21 |
parent 12552 | d2d2ab3f1f37 |
child 12667 | 7e6eaaa125f2 |
--- 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