--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/epsilon.thy	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,18 @@
+(*  Title: 	ZF/epsilon.thy
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+Epsilon induction and recursion
+*)
+
+Epsilon = Nat +
+consts
+    eclose,rank ::      "i=>i"
+    transrec    ::      "[i, [i,i]=>i] =>i"
+
+rules
+  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))"
+end