# HG changeset patch
# User paulson
# Date 902239519 -7200
# Node ID e5129172cb2b7bf989ded5ee5364b543f7413e77
# Parent  bbcd79ef7cf25d167fe80ff630f881b45f349e54
Renamed equals0D to equals0E; tidied

diff -r bbcd79ef7cf2 -r e5129172cb2b src/ZF/AC/AC16_WO4.ML
--- a/src/ZF/AC/AC16_WO4.ML	Tue Aug 04 10:50:33 1998 +0200
+++ b/src/ZF/AC/AC16_WO4.ML	Tue Aug 04 16:05:19 1998 +0200
@@ -61,7 +61,7 @@
         equals0I, HartogI RSN (2, lepoll_trans1),
         subset_imp_lepoll RS (paired_eqpoll RS eqpoll_sym RS
         eqpoll_imp_lepoll RSN (2, lepoll_trans))]
-        addSEs [RepFunE, nat_not_Finite RS notE] addEs [mem_asym]
+        addSEs [nat_not_Finite RS notE] addEs [mem_asym]
         addSDs [Un_upper1 RS subset_imp_lepoll RS lepoll_Finite,
         paired_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll
         RS lepoll_Finite]) 1);
@@ -162,7 +162,7 @@
 
 Goal "[| a eqpoll k; a<=y; b:y-a; u:x; x Int y = 0  \
 \       |] ==> cons(b, cons(u, a)) eqpoll succ(succ(k))";
-by (fast_tac (claset() addSIs [cons_eqpoll_succ] addEs [equals0D]) 1);
+by (fast_tac (claset() addSIs [cons_eqpoll_succ] addEs [equals0E]) 1);
 qed "cons_cons_eqpoll";
 
 Goalw [s_u_def] "s_u(u, t_n, k, y) <= t_n";
@@ -348,7 +348,7 @@
 
 Goal "[| x Int y = 0; w <= x Un y |]  \
 \        ==> w Int (x - {u}) = w - cons(u, w Int y)";
-by (fast_tac (claset() addEs [equals0D]) 1);
+by (fast_tac (claset() addEs [equals0E]) 1);
 qed "w_Int_eq_w_Diff";
 
 Goal "[| w:{v:s_u(u, t_n, succ(l), y). a <= v};  \
@@ -359,7 +359,7 @@
 by (etac CollectE 1);
 by (resolve_tac [w_Int_eq_w_Diff RS ssubst] 1 THEN (assume_tac 1));
 by (fast_tac (claset() addSDs [s_u_subset RS subsetD]) 1);
-by (fast_tac (claset() addEs [equals0D] addSDs [bspec]
+by (fast_tac (claset() addEs [equals0E] addSDs [bspec]
         addDs [s_u_subset RS subsetD]
         addSEs [eqpoll_sym RS cons_eqpoll_succ RS eqpoll_sym, in_s_u_imp_u_in]
         addSIs [eqpoll_sum_imp_Diff_eqpoll]) 1);
@@ -373,7 +373,7 @@
 Goal
         "[| z : xa Int (x - {u}); l eqpoll a; a <= y; x Int y = 0; u:x  \
 \       |] ==> cons(z, cons(u, a)) : {v: Pow(x Un y). v eqpoll succ(succ(l))}";
-by (fast_tac (claset() addSIs [cons_eqpoll_succ] addEs [equals0D, eqpoll_sym]) 1);
+by (fast_tac (claset() addSIs [cons_eqpoll_succ] addEs [equals0E, eqpoll_sym]) 1);
 qed "cons_cons_in";
 
 (* ********************************************************************** *)
@@ -505,9 +505,9 @@
 Goalw [LL_def, MM_def]
         "t_n <= {v:Pow(x Un y). v eqpoll n}  \
 \               ==> LL(t_n, k, y) <= {z:Pow(y). z lepoll n}";
-by (fast_tac (claset() addSEs [RepFunE]
-        addIs [subset_imp_lepoll RS (eqpoll_imp_lepoll
-                RSN (2, lepoll_trans))]) 1);
+by (fast_tac (claset() addIs [subset_imp_lepoll 
+			      RS (eqpoll_imp_lepoll
+				  RSN (2, lepoll_trans))]) 1);
 qed "LL_subset";
 
 Goal "[| t_n <= {v:Pow(x Un y). v eqpoll n}; \
@@ -527,7 +527,7 @@
 \       t_n <= {v:Pow(x Un y). v eqpoll n}; \
 \       v:LL(t_n, k, y)  \
 \       |] ==> EX! w. w:MM(t_n, k, y) & v<=w";
-by (safe_tac (claset() addSEs [RepFunE]));
+by Safe_tac;
 by (Fast_tac 1);
 by (resolve_tac [lepoll_imp_eqpoll_subset RS exE] 1 THEN (assume_tac 1));
 by (eres_inst_tac [("x","xa")] ballE 1);
@@ -583,7 +583,7 @@
 by (asm_full_simp_tac (simpset() delsimps ball_simps addsimps [Int_in_LL]) 1);
 by (eresolve_tac [unique_superset_in_MM RS the_equality2 RS ssubst] 1
         THEN (assume_tac 1));
-by (REPEAT (fast_tac (claset() addEs [equals0D] addSEs [Int_in_LL]) 1));
+by (REPEAT (fast_tac (claset() addEs [equals0E] addSEs [Int_in_LL]) 1));
 qed "exists_in_LL";
 
 Goalw [LL_def] 
diff -r bbcd79ef7cf2 -r e5129172cb2b src/ZF/AC/AC17_AC1.ML
--- a/src/ZF/AC/AC17_AC1.ML	Tue Aug 04 10:50:33 1998 +0200
+++ b/src/ZF/AC/AC17_AC1.ML	Tue Aug 04 16:05:19 1998 +0200
@@ -61,8 +61,7 @@
 
 Goal "[| f`Z : Z; Z:Pow(x)-{0} |] ==>  \
 \       (lam X:Pow(x)-{0}. {f`X})`Z : Pow(Z)-{0}";
-by (Asm_full_simp_tac 1);
-by (fast_tac (claset() addSDs [equals0D]) 1);
+by Auto_tac;
 val lemma3 = result();
 
 Goal "EX f:F. f`((lam f:F. Q(f))`f) : (lam f:F. Q(f))`f  \
diff -r bbcd79ef7cf2 -r e5129172cb2b src/ZF/AC/AC18_AC19.ML
--- a/src/ZF/AC/AC18_AC19.ML	Tue Aug 04 10:50:33 1998 +0200
+++ b/src/ZF/AC/AC18_AC19.ML	Tue Aug 04 16:05:19 1998 +0200
@@ -25,14 +25,13 @@
 by (rtac subsetI 1);
 by (eres_inst_tac [("x","{{b:B(a). x:X(a,b)}. a:A}")] allE 1);
 by (etac impE 1);
-by (fast_tac (claset() addSEs [RepFunE] addSDs [INT_E]
-                addEs [UN_E, sym RS equals0D]) 1);
+by (fast_tac (claset() addEs [sym RS equals0E]) 1);
 by (etac exE 1);
 by (rtac UN_I 1);
 by (fast_tac (claset() addSEs [PROD_subsets]) 1);
 by (Simp_tac 1);
 by (fast_tac (claset() addSEs [not_emptyE] addDs [RepFunI RSN (2, apply_type)]
-                addEs [CollectD2] addSIs [INT_I]) 1);
+	      ) 1);
 qed "lemma_AC18";
 
 val [prem] = goalw thy (AC18_def::AC_defs) "AC1 ==> AC18";
@@ -57,8 +56,8 @@
 
 Goalw [u_def]
         "[| A ~= 0; 0 ~: A |] ==> {u_(a). a:A} ~= 0 & 0 ~: {u_(a). a:A}";
-by (fast_tac (claset() addSIs [not_emptyI, RepFunI]
-                addSEs [not_emptyE, RepFunE]
+by (fast_tac (claset() addSIs [not_emptyI]
+                addSEs [not_emptyE]
                 addSDs [sym RS (RepFun_eq_0_iff RS iffD1)]) 1);
 qed "RepRep_conj";
 
@@ -76,8 +75,7 @@
 Goalw [u_def]
         "[| f`(u_(a)) ~: a; f: (PROD B:{u_(a). a:A}. B); a:A |]  \
 \               ==> f`(u_(a))-{0} : a";
-by (fast_tac (claset() addSEs [RepFunI, RepFunE, lemma1_1]
-                addSDs [apply_type]) 1);
+by (fast_tac (claset() addSEs [lemma1_1] addSDs [apply_type]) 1);
 val lemma1_2 = result();
 
 Goal  "EX f. f: (PROD B:{u_(a). a:A}. B) ==> EX f. f: (PROD B:A. B)";
@@ -98,7 +96,7 @@
 Goal "[| A~=0; 0~:A |] ==> (INT x:{u_(a). a:A}. UN b:x. b) ~= 0";
 by (etac not_emptyE 1);
 by (res_inst_tac [("a","0")] not_emptyI 1);
-by (fast_tac (claset() addSIs [INT_I, RepFunI, lemma2_1] addSEs [RepFunE]) 1);
+by (fast_tac (claset() addSIs [lemma2_1]) 1);
 val lemma2 = result();
 
 Goal "(UN f:F. P(f)) ~= 0 ==> F ~= 0";
diff -r bbcd79ef7cf2 -r e5129172cb2b src/ZF/AC/AC1_WO2.ML
--- a/src/ZF/AC/AC1_WO2.ML	Tue Aug 04 10:50:33 1998 +0200
+++ b/src/ZF/AC/AC1_WO2.ML	Tue Aug 04 16:05:19 1998 +0200
@@ -13,7 +13,7 @@
 by (resolve_tac [bij_Least_HH_x RS bij_converse_bij] 1);
 by (rtac f_subsets_imp_UN_HH_eq_x 1);
 by (resolve_tac [lam_type RS apply_type] 1 THEN (assume_tac 2));
-by (fast_tac (claset() addSDs [equals0D, prem RS apply_type]) 1);
+by (fast_tac (claset() addSEs [equals0E] addSDs [prem RS apply_type]) 1);
 by (fast_tac (claset() addSIs [prem RS Pi_weaken_type]) 1);
 val lemma1 = uresult() |> standard;
 
diff -r bbcd79ef7cf2 -r e5129172cb2b src/ZF/AC/AC2_AC6.ML
--- a/src/ZF/AC/AC2_AC6.ML	Tue Aug 04 10:50:33 1998 +0200
+++ b/src/ZF/AC/AC2_AC6.ML	Tue Aug 04 16:05:19 1998 +0200
@@ -21,7 +21,7 @@
 
 Goalw [pairwise_disjoint_def]
         "[| pairwise_disjoint(A); B:A; C:A; D:B; D:C |] ==> f`B = f`C";
-by (fast_tac (claset() addSEs [equals0D]) 1);
+by (fast_tac (claset() addSEs [equals0E]) 1);
 val lemma2 = result();
 
 Goalw AC_defs "AC1 ==> AC2"; 
@@ -30,7 +30,7 @@
 by (REPEAT (eresolve_tac [asm_rl,conjE,allE,exE,impE] 1));
 by (REPEAT (resolve_tac [exI,ballI,equalityI] 1));
 by (rtac lemma1 2 THEN (REPEAT (assume_tac 2)));
-by (fast_tac (claset() addSEs [RepFunE, lemma2] addEs [apply_type]) 1);
+by (fast_tac (claset() addSEs [lemma2] addEs [apply_type]) 1);
 qed "AC1_AC2";
 
 
@@ -40,7 +40,7 @@
 
 Goal "0~:A ==> 0 ~: {B*{B}. B:A}";
 by (fast_tac (claset() addSDs [sym RS (Sigma_empty_iff RS iffD1)]
-        addSEs [RepFunE, equals0D]) 1);
+        addSEs [equals0E]) 1);
 val lemma1 = result();
 
 Goal "[| X*{X} Int C = {y}; X:A |]  \
@@ -72,7 +72,7 @@
 (* ********************************************************************** *)
 
 Goal "0 ~: {R``{x}. x:domain(R)}";
-by (fast_tac (claset() addEs [sym RS equals0D]) 1);
+by (fast_tac (claset() addEs [sym RS equals0E]) 1);
 val lemma = result();
 
 Goalw AC_defs "AC1 ==> AC4";
@@ -194,6 +194,6 @@
 (* ********************************************************************** *)
 
 Goalw AC_defs "AC1 <-> AC6";
-by (fast_tac (claset() addDs [equals0D] addSEs [not_emptyE]) 1);
+by (blast_tac (claset() addEs [equals0E]) 1);
 qed "AC1_iff_AC6";
 
diff -r bbcd79ef7cf2 -r e5129172cb2b src/ZF/AC/AC7_AC9.ML
--- a/src/ZF/AC/AC7_AC9.ML	Tue Aug 04 10:50:33 1998 +0200
+++ b/src/ZF/AC/AC7_AC9.ML	Tue Aug 04 16:05:19 1998 +0200
@@ -20,7 +20,7 @@
 Goal "[| 0~:A; B:A |] ==> (nat->Union(A))*B ~= 0";
 by (fast_tac (claset() addSDs [Sigma_empty_iff RS iffD1]
                 addDs [fun_space_emptyD, mem_not_eq_not_mem]
-                addEs [equals0D]
+                addEs [equals0E]
                 addSIs [equals0I,UnionI]) 1);
 qed "Sigma_fun_space_not0";
 
@@ -105,12 +105,11 @@
 Goal "(PROD B:{(nat->Union(A))*C. C:A}. B) ~= 0  \
 \               ==> (PROD B:A. B) ~= 0";
 by (fast_tac (claset() addSIs [equals0I,lemma1_1, lemma1_2]
-                addSEs [equals0D]) 1);
+                addSEs [equals0E]) 1);
 val lemma1 = result();
 
 Goal "0 ~: A ==> 0 ~: {(nat -> Union(A)) * C. C:A}";
-by (fast_tac (claset() addEs [RepFunE,
-                Sigma_fun_space_not0 RS not_sym RS notE]) 1);
+by (fast_tac (claset() addEs [Sigma_fun_space_not0 RS not_sym RS notE]) 1);
 val lemma2 = result();
 
 Goalw AC_defs "AC7 ==> AC6";
@@ -121,9 +120,8 @@
 by (rtac lemma1 1);
 by (etac allE 1);
 by (etac impE 1 THEN (assume_tac 2));
-by (fast_tac (claset() addSEs [RepFunE]
-        addSIs [lemma2, all_eqpoll_imp_pair_eqpoll,
-                Sigma_fun_space_eqpoll]) 1);
+by (fast_tac (claset() addSIs [lemma2, all_eqpoll_imp_pair_eqpoll,
+			       Sigma_fun_space_eqpoll]) 1);
 qed "AC7_AC6";
 
 
@@ -134,26 +132,17 @@
 Goalw [eqpoll_def]
         "ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2  \
 \       ==> 0 ~: { bij(fst(B),snd(B)). B:A }";
-by (rtac notI 1);
-by (etac RepFunE 1);
-by (dtac bspec 1 THEN (assume_tac 1));
-by (REPEAT (eresolve_tac [exE,conjE] 1));
-by (hyp_subst_tac 1);
-by (Asm_full_simp_tac 1);
+by Auto_tac;
 val lemma1 = result();
 
-Goal "[| f: (PROD X:RepFun(A,p). X); D:A |]  \
-\               ==> (lam x:A. f`p(x))`D : p(D)";
+Goal "[| f: (PROD X:RepFun(A,p). X); D:A |] ==> (lam x:A. f`p(x))`D : p(D)";
 by (resolve_tac [beta RS ssubst] 1 THEN (assume_tac 1));
 by (fast_tac (claset() addSEs [apply_type]) 1);
 val lemma2 = result();
 
 Goalw AC_defs "AC1 ==> AC8";
-by (rtac allI 1);
-by (etac allE 1);
-by (rtac impI 1);
-by (etac impE 1);
-by (etac lemma1 1);
+by (Clarify_tac 1);
+by (dtac lemma1 1);
 by (fast_tac (claset() addSEs [lemma2]) 1);
 qed "AC1_AC8";
 
diff -r bbcd79ef7cf2 -r e5129172cb2b src/ZF/AC/AC_Equiv.ML
--- a/src/ZF/AC/AC_Equiv.ML	Tue Aug 04 10:50:33 1998 +0200
+++ b/src/ZF/AC/AC_Equiv.ML	Tue Aug 04 16:05:19 1998 +0200
@@ -39,7 +39,7 @@
 (* ********************************************************************** *)
 
 Goal "(A->X)=0 ==> X=0";
-by (fast_tac (claset() addSIs [equals0I] addEs [lam_type RSN (2, equals0D)]) 1);
+by (fast_tac (claset() addSIs [equals0I] addEs [lam_type RSN (2, equals0E)]) 1);
 qed "fun_space_emptyD";
 
 (* used only in WO1_DC.ML *)
@@ -119,7 +119,7 @@
 qed "inj_strengthen_type";
 
 Goal "A*B=0 <-> A=0 | B=0";
-by (fast_tac (claset() addSIs [equals0I] addEs [equals0D]) 1);
+by (fast_tac (claset() addSIs [equals0I] addEs [equals0E]) 1);
 qed "Sigma_empty_iff";
 
 Goalw [Finite_def] "n:nat ==> Finite(n)";
diff -r bbcd79ef7cf2 -r e5129172cb2b src/ZF/AC/Cardinal_aux.ML
--- a/src/ZF/AC/Cardinal_aux.ML	Tue Aug 04 10:50:33 1998 +0200
+++ b/src/ZF/AC/Cardinal_aux.ML	Tue Aug 04 16:05:19 1998 +0200
@@ -185,16 +185,6 @@
 by (eresolve_tac [Ord_Least RSN (2, ltI)] 1);
 qed "UN_eq_UN_Diffs";
 
-Goalw [eqpoll_def] "A Int B = 0 ==> A Un B eqpoll A + B";
-by (res_inst_tac [("x","lam a:A Un B. if(a:A,Inl(a),Inr(a))")] exI 1);
-by (res_inst_tac [("d","%z. case(%x. x, %x. x, z)")] lam_bijective 1);
-by (fast_tac (claset() addSIs [if_type, InlI, InrI]) 1);
-by (TRYALL (etac sumE ));
-by (TRYALL (split_tac [split_if]));
-by (TRYALL Asm_simp_tac);
-by (fast_tac (claset() addDs [equals0D]) 1);
-qed "disj_Un_eqpoll_sum";
-
 Goalw [lepoll_def, eqpoll_def]
         "a lepoll X ==> EX Y. Y<=X & a eqpoll Y";
 by (etac exE 1);
diff -r bbcd79ef7cf2 -r e5129172cb2b src/ZF/AC/DC.ML
--- a/src/ZF/AC/DC.ML	Tue Aug 04 10:50:33 1998 +0200
+++ b/src/ZF/AC/DC.ML	Tue Aug 04 16:05:19 1998 +0200
@@ -572,11 +572,10 @@
 qed "lam_type_RepFun";
 
 Goal "[| ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y, x> : R);  \
-\       b:a; Z:Pow(X); Z lesspoll a |]  \
-\       ==> {x:X. <Z,x> : R} ~= 0";
-by (fast_tac (FOL_cs addEs [bexE, equals0D]
-        addSDs [bspec] addIs [CollectI]) 1);
-val lemma_ = result();
+\        b:a; Z:Pow(X); Z lesspoll a |]  \
+\     ==> {x:X. <Z,x> : R} ~= 0";
+by (blast_tac (claset() addEs [equals0E]) 1);
+val lemmaX = result();
 
 Goal "[| Card(K); well_ord(X,Q);  \
 \       ALL Y:Pow(X). Y lesspoll K --> (EX x:X. <Y, x> : R); b:K |]  \
@@ -590,11 +589,10 @@
 by (Fast_tac 1);
 by (asm_full_simp_tac (simpset()
         addsimps [[lam_type_RepFun, subset_refl] MRS image_fun]) 1);
-by (etac lemma_ 1 THEN (assume_tac 1));
-by (fast_tac (claset() addSEs [RepFunE, impE, notE]
-                addEs [Card_is_Ord RSN (2, OrdmemD) RS subsetD]) 1);
+by (etac lemmaX 1 THEN assume_tac 1);
+by (blast_tac (claset() addIs [Card_is_Ord RSN (2, OrdmemD) RS subsetD]) 1);
 by (fast_tac (claset() addSEs [[in_Card_imp_lesspoll, RepFun_lepoll]
-                MRS lepoll_lesspoll_lesspoll]) 1);
+			       MRS lepoll_lesspoll_lesspoll]) 1);
 val lemma = result();
 
 Goalw [DC_def, WO1_def]
diff -r bbcd79ef7cf2 -r e5129172cb2b src/ZF/AC/DC_lemmas.ML
--- a/src/ZF/AC/DC_lemmas.ML	Tue Aug 04 10:50:33 1998 +0200
+++ b/src/ZF/AC/DC_lemmas.ML	Tue Aug 04 16:05:19 1998 +0200
@@ -10,7 +10,7 @@
         "Ord(a) ==> {P(b). b:a} lepoll a";
 by (res_inst_tac [("x","lam z:RepFun(a,P). LEAST i. z=P(i)")] exI 1);
 by (res_inst_tac [("d","%z. P(z)")] (sym RSN (2, lam_injective)) 1);
-by (fast_tac (claset() addSEs [RepFunE] addSIs [Least_in_Ord, prem]) 1);
+by (fast_tac (claset() addSIs [Least_in_Ord, prem]) 1);
 by (REPEAT (eresolve_tac [RepFunE, LeastI, prem RS Ord_in_Ord] 1));
 qed "RepFun_lepoll";
 
diff -r bbcd79ef7cf2 -r e5129172cb2b src/ZF/AC/HH.ML
--- a/src/ZF/AC/HH.ML	Tue Aug 04 10:50:33 1998 +0200
+++ b/src/ZF/AC/HH.ML	Tue Aug 04 16:05:19 1998 +0200
@@ -151,8 +151,7 @@
 qed "lam_surj_sing";
 
 Goal "y:Pow(x)-{0} ==> x ~= 0";
-by (fast_tac (claset() addSIs [equals0I, singletonI RS subst_elem]
-                addSDs [equals0D]) 1);
+by Auto_tac;
 qed "not_emptyI2";
 
 Goal "f`(x - (UN j:i. HH(f,x,j))): Pow(x - (UN j:i. HH(f,x,j)))-{0}  \
diff -r bbcd79ef7cf2 -r e5129172cb2b src/ZF/AC/WO1_AC.ML
--- a/src/ZF/AC/WO1_AC.ML	Tue Aug 04 10:50:33 1998 +0200
+++ b/src/ZF/AC/WO1_AC.ML	Tue Aug 04 16:05:19 1998 +0200
@@ -44,7 +44,7 @@
 by (eres_inst_tac [("x","Union({{C:D(B). P(C,B)}. B:A})")] allE 1);
 by (etac exE 1);
 by (dtac ex_choice_fun 1);
-by (fast_tac (claset() addEs [RepFunE, sym RS equals0D]) 1);
+by (fast_tac (claset() addEs [sym RS equals0E]) 1);
 by (etac exE 1);
 by (res_inst_tac [("x","lam x:A. f`{C:D(x). P(C,x)}")] exI 1);
 by (Asm_full_simp_tac 1);
@@ -69,8 +69,7 @@
 val lemma2_1 = result();
 
 Goal "f : bij(D+D, B) ==> {{f`Inl(i), f`Inr(i)}. i:D} : Pow(Pow(B))";
-by (fast_tac (claset() addSIs [InlI, InrI]
-                addSEs [RepFunE, bij_is_fun RS apply_type]) 1);
+by (fast_tac (claset() addSEs [bij_is_fun RS apply_type]) 1);
 val lemma2_2 = result();
 
 Goal "[| f:inj(A,B); f`a = f`b; a:A; b:A |] ==> a=b";
@@ -79,13 +78,8 @@
 val lemma = result();
 
 Goalw AC_aux_defs
-        "f : bij(D+D, B) ==>  \
-\               pairwise_disjoint({{f`Inl(i), f`Inr(i)}. i:D})";
-by (fast_tac (claset() addSEs [RepFunE, not_emptyE] 
-        addDs [bij_is_inj RS lemma, Inl_iff RS iffD1,
-                Inr_iff RS iffD1, Inl_Inr_iff RS iffD1 RS FalseE,
-                Inr_Inl_iff RS iffD1 RS FalseE]
-        addSIs [InlI, InrI]) 1);
+        "f : bij(D+D, B) ==> pairwise_disjoint({{f`Inl(i), f`Inr(i)}. i:D})";
+by (blast_tac (claset() addDs [bij_is_inj RS lemma]) 1);
 val lemma2_3 = result();
 
 val [major, minor] = goalw thy AC_aux_defs 
@@ -93,11 +87,11 @@
 \       sets_of_size_between({{f`Inl(i), f`Inr(i)}. i:D}, 2, succ(n))";
 by (rewtac succ_def);
 by (fast_tac (claset() 
-        addSIs [cons_lepoll_cong, minor, lepoll_refl, InlI, InrI] 
+        addSIs [cons_lepoll_cong, minor, lepoll_refl] 
         addIs [singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans,
                 le_imp_subset RS subset_imp_lepoll]
-        addDs [major RS bij_is_inj RS lemma, Inl_Inr_iff RS iffD1 RS FalseE]
-        addSEs [RepFunE, not_emptyE, mem_irrefl]) 1);
+        addDs [major RS bij_is_inj RS lemma]
+        addSEs [mem_irrefl]) 1);
 val lemma2_4 = result();
 
 Goalw [bij_def, surj_def]
diff -r bbcd79ef7cf2 -r e5129172cb2b src/ZF/AC/WO1_WO7.ML
--- a/src/ZF/AC/WO1_WO7.ML	Tue Aug 04 10:50:33 1998 +0200
+++ b/src/ZF/AC/WO1_WO7.ML	Tue Aug 04 16:05:19 1998 +0200
@@ -49,9 +49,7 @@
     THEN (assume_tac 1));
 by (rtac notI 1);
 by (eres_inst_tac [("x","nat")] allE 1);
-by (etac disjE 1);
-by (fast_tac (claset() addSDs [nat_0I RSN (2,equals0D)]) 1);
-by (Blast_tac 1);
+by (blast_tac (claset() addSEs [nat_0I RSN (2,equals0E)]) 1);
 qed "converse_Memrel_not_wf_on";
 
 Goalw [well_ord_def] 
diff -r bbcd79ef7cf2 -r e5129172cb2b src/ZF/AC/WO2_AC16.ML
--- a/src/ZF/AC/WO2_AC16.ML	Tue Aug 04 10:50:33 1998 +0200
+++ b/src/ZF/AC/WO2_AC16.ML	Tue Aug 04 16:05:19 1998 +0200
@@ -378,7 +378,7 @@
 
 
 Goal "[| A <= B Un C; A Int C = 0 |] ==> A <= B";
-by (fast_tac (claset() addDs [equals0D]) 1);
+by (fast_tac (claset() addEs [equals0E]) 1);
 qed "subset_Un_disjoint";
 
 
diff -r bbcd79ef7cf2 -r e5129172cb2b src/ZF/AC/WO6_WO1.ML
--- a/src/ZF/AC/WO6_WO1.ML	Tue Aug 04 10:50:33 1998 +0200
+++ b/src/ZF/AC/WO6_WO1.ML	Tue Aug 04 16:05:19 1998 +0200
@@ -375,7 +375,7 @@
 (* ********************************************************************** *)
 
 Goalw [WO6_def, NN_def] "!!y. WO6 ==> NN(y) ~= 0";
-by (fast_tac (ZF_cs addEs [equals0D]) 1);
+by (fast_tac (ZF_cs addEs [equals0E]) 1);
 qed "WO6_imp_NN_not_empty";
 
 (* ********************************************************************** *)