--- a/src/ZF/AC/AC10_AC15.ML Wed Jul 26 16:23:42 1995 +0200
+++ b/src/ZF/AC/AC10_AC15.ML Wed Jul 26 17:35:23 1995 +0200
@@ -110,9 +110,9 @@
\ sets_of_size_between(f`B, 2, succ(n)) & \
\ Union(f`B)=B; n:nat |] \
\ ==> EX f. ALL B:A. f`B ~= 0 & f`B <= B & f`B lepoll n";
-by (fast_tac (empty_cs addSDs [lemma3, bspec, theI]
+by (fast_tac (empty_cs addSDs [lemma3, theI] addDs [bspec]
addSEs [exE, conjE]
- addSIs [exI, ballI, lemma5]) 1);
+ addIs [exI, ballI, lemma5]) 1);
val ex_fun_AC13_AC15 = result();
(* ********************************************************************** *)
@@ -170,7 +170,7 @@
by (safe_tac ZF_cs);
by (fast_tac (empty_cs addSEs [allE, cons_times_nat_not_Finite RSN (2, impE),
ex_fun_AC13_AC15]) 1);
-val AC10_imp_AC13 = result();
+qed "AC10_AC13";
(* ********************************************************************** *)
(* The proofs needed in the second case, not in the first *)
@@ -246,12 +246,12 @@
goalw thy AC_defs "!!Z. AC13(1) ==> AC1";
by (fast_tac (AC_cs addSEs [lemma]) 1);
-qed "AC13(1)_AC1";
+qed "AC13_AC1";
(* ********************************************************************** *)
(* AC11 ==> AC14 *)
(* ********************************************************************** *)
goalw thy [AC11_def, AC14_def] "!!Z. AC11 ==> AC14";
-by (fast_tac (ZF_cs addSIs [AC10_imp_AC13]) 1);
+by (fast_tac (ZF_cs addSIs [AC10_AC13]) 1);
qed "AC11_AC14";