diff -r 1748c16c2df3 -r 249600a63ba9 src/ZF/AC/recfunAC16.thy
--- a/src/ZF/AC/recfunAC16.thy	Wed Jan 16 15:04:37 2002 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  Title:      ZF/AC/recfunAC16.thy
-    ID:         $Id$
-    Author:     Krzysztof Grabczewski
-
-A recursive definition used in the proof of WO2 ==> AC16
-*)
-
-recfunAC16 = Cardinal + Epsilon +
-
-constdefs
-  recfunAC16 :: [i, i, i, i] => i
-
-    "recfunAC16(f,fa,i,a) == 
-         transrec2(i, 0, 
-              %g r. if(\\<exists>y \\<in> r. fa`g \\<subseteq> y, r, 
-                       r Un {f`(LEAST i. fa`g \\<subseteq> f`i & 
-                       (\\<forall>b<a. (fa`b \\<subseteq> f`i --> (\\<forall>t \\<in> r. ~ fa`b \\<subseteq> t))))}))"
-
-end