# HG changeset patch
# User paulson
# Date 905442164 -7200
# Node ID 855654b691db60b64324cbb9cc3db933926efcfd
# Parent  024d887eae506d0954009fe14894c4438227e6e0
eliminated equals0E

diff -r 024d887eae50 -r 855654b691db src/ZF/AC/AC16_WO4.ML
--- a/src/ZF/AC/AC16_WO4.ML	Thu Sep 10 17:42:02 1998 +0200
+++ b/src/ZF/AC/AC16_WO4.ML	Thu Sep 10 17:42:44 1998 +0200
@@ -256,7 +256,7 @@
 AddSIs [Infinite];   (*if notI is removed!*)
 AddSEs [Infinite RS notE];
 
-AddEs [IntI RS (disjoint RS equals0E)];
+AddEs [[disjoint, IntI] MRS (equals0D RS notE)];
 
 (*use k = succ(l) *)
 val includes_l = simplify (FOL_ss addsimps [k_def]) includes;
diff -r 024d887eae50 -r 855654b691db src/ZF/AC/AC1_WO2.ML
--- a/src/ZF/AC/AC1_WO2.ML	Thu Sep 10 17:42:02 1998 +0200
+++ b/src/ZF/AC/AC1_WO2.ML	Thu Sep 10 17:42:44 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() addSEs [equals0E] addSDs [prem RS apply_type]) 1);
+by (fast_tac (claset() addSDs [prem RS apply_type]) 1);
 by (fast_tac (claset() addSIs [prem RS Pi_weaken_type]) 1);
 val lemma1 = uresult() |> standard;
 
diff -r 024d887eae50 -r 855654b691db src/ZF/AC/AC7_AC9.ML
--- a/src/ZF/AC/AC7_AC9.ML	Thu Sep 10 17:42:02 1998 +0200
+++ b/src/ZF/AC/AC7_AC9.ML	Thu Sep 10 17:42:44 1998 +0200
@@ -91,8 +91,7 @@
 val lemma1_2 = result();
 
 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 [equals0E]) 1);
+by (fast_tac (claset() addSIs [equals0I,lemma1_1, lemma1_2]) 1);
 val lemma1 = result();
 
 Goal "0 ~: A ==> 0 ~: {(nat -> Union(A)) * C. C:A}";
diff -r 024d887eae50 -r 855654b691db src/ZF/AC/AC_Equiv.ML
--- a/src/ZF/AC/AC_Equiv.ML	Thu Sep 10 17:42:02 1998 +0200
+++ b/src/ZF/AC/AC_Equiv.ML	Thu Sep 10 17:42:44 1998 +0200
@@ -39,7 +39,7 @@
 (* ********************************************************************** *)
 
 Goal "(A->X)=0 ==> X=0";
-by (fast_tac (claset() addSIs [equals0I] addEs [lam_type RSN (2, equals0E)]) 1);
+by (fast_tac (claset() addSIs [equals0I] addIs [lam_type]) 1);
 qed "fun_space_emptyD";
 
 (* used only in WO1_DC.ML *)