--- a/src/ZF/epsilon.thy Sat Apr 05 16:18:58 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(* 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 + "mono" +
-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