--- 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]
--- 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 \
--- 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";
--- 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;
--- 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";
--- 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";
--- 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)";
--- 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);
--- 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]
--- 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";
--- 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} \
--- 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]
--- 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]
--- 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";
--- 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";
(* ********************************************************************** *)