changeset 753 | ec86863e87c8 |
parent 124 | 858ab9a9b047 |
child 1401 | 0c439768f45c |
--- a/src/ZF/Epsilon.thy Mon Nov 28 19:48:30 1994 +0100 +++ b/src/ZF/Epsilon.thy Tue Nov 29 00:31:31 1994 +0100 @@ -11,7 +11,7 @@ eclose,rank :: "i=>i" transrec :: "[i, [i,i]=>i] =>i" -rules +defs eclose_def "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))" transrec_def "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)" rank_def "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"