src/ZF/Epsilon.thy
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))"