src/ZF/AC/AC1_AC17.ML

--- a/src/ZF/AC/AC1_AC17.ML	Tue Jun 26 15:28:49 2001 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(*  Title:      ZF/AC/AC1_AC17.ML
-    ID:         $Id$
-    Author:     Krzysztof Grabczewski
-
-The proof of AC1 ==> AC17
-*)
-
-Goal "f \\<in> (\\<Pi>X \\<in> Pow(A) - {0}. X) ==> f \\<in> (Pow(A) - {0} -> A)";
-by (rtac Pi_type 1 THEN (assume_tac 1));
-by (dtac apply_type 1 THEN (assume_tac 1));
-by (Fast_tac 1);
-val lemma1 = result();
-
-Goalw AC_defs "AC1 ==> AC17";
-by (rtac allI 1);
-by (rtac ballI 1);
-by (eres_inst_tac [("x","Pow(A)-{0}")] allE 1);
-by (etac impE 1);
-by (Fast_tac 1);
-by (etac exE 1);
-by (rtac bexI 1);
-by (etac lemma1 2);
-by (rtac apply_type 1 THEN (assume_tac 1));
-by (fast_tac (claset() addSDs [lemma1] addSEs [apply_type]) 1);
-qed "AC1_AC17";