--- a/src/ZF/AC/WO_AC.ML Wed Jan 16 15:04:37 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(* Title: ZF/AC/WO_AC.ML
- ID: $Id$
- Author: Krzysztof Grabczewski
-
-Lemmas used in the proofs like WO? ==> AC?
-*)
-
-Goal "[| well_ord(Union(A),r); 0\\<notin>A; B \\<in> A |] \
-\ ==> (THE b. first(b,B,r)) \\<in> B";
-by (fast_tac (claset() addSEs [well_ord_imp_ex1_first RS theI RS
- (first_def RS def_imp_iff RS iffD1 RS conjunct1)]) 1);
-qed "first_in_B";
-
-Goal "[| well_ord(Union(A), R); 0\\<notin>A |] ==> \\<exists>f. f:(\\<Pi>X \\<in> A. X)";
-by (fast_tac (claset() addSEs [first_in_B] addSIs [lam_type]) 1);
-qed "ex_choice_fun";
-
-Goal "well_ord(A, R) ==> \\<exists>f. f:(\\<Pi>X \\<in> Pow(A)-{0}. X)";
-by (fast_tac (claset() addSEs [well_ord_subset RS ex_choice_fun]) 1);
-qed "ex_choice_fun_Pow";