Corrected for new classical reasoner: redundant rules
are now ignored, even if this could increase their priority

--- a/src/ZF/AC/AC0_AC1.ML	Mon Aug 19 15:35:11 1996 +0200
+++ b/src/ZF/AC/AC0_AC1.ML	Tue Aug 20 12:23:13 1996 +0200
@@ -19,5 +19,8 @@
 qed "AC0_AC1";
 
 goalw thy AC_defs "!!Z. AC1 ==> AC0";
-by (fast_tac (FOL_cs addSIs [notI, singletonI] addSEs [notE, DiffE]) 1);
+by (deepen_tac ZF_cs 0 1);
+(*Large search space.  Faster proof by
+  by (fast_tac (FOL_cs addSIs [notI, singletonI] addSEs [notE, DiffE]) 1);
+*)
 qed "AC1_AC0";

--- a/src/ZF/AC/AC16_WO4.ML	Mon Aug 19 15:35:11 1996 +0200
+++ b/src/ZF/AC/AC16_WO4.ML	Tue Aug 20 12:23:13 1996 +0200
@@ -440,8 +440,7 @@
 
 goal thy "{x:Pow(X). x lepoll 0} = {0}";
 by (fast_tac (AC_cs addSDs [lepoll_0_is_0]
-                addSIs [singletonI, lepoll_refl, equalityI]
-                addSEs [singletonE]) 1);
+                    addSIs [lepoll_refl, equalityI]) 1);
 val subsets_lepoll_0_eq_unit = result();
 
 goal thy "!!X. [| well_ord(X, R); ~Finite(X); n:nat |]  \

--- a/src/ZF/AC/AC2_AC6.ML	Mon Aug 19 15:35:11 1996 +0200
+++ b/src/ZF/AC/AC2_AC6.ML	Tue Aug 20 12:23:13 1996 +0200
@@ -72,13 +72,13 @@
 (* ********************************************************************** *)
 
 goal thy "!!R. 0 ~: {R``{x}. x:domain(R)}";
-by (fast_tac (AC_cs addSEs [RepFunE, domainE, sym RS equals0D]) 1);
+by (fast_tac (AC_cs addEs [sym RS equals0D]) 1);
 val lemma = result();
 
 goalw thy AC_defs "!!Z. AC1 ==> AC4";
 by (REPEAT (resolve_tac [allI, impI] 1));
 by (REPEAT (eresolve_tac [allE, lemma RSN (2, impE), exE] 1));
-by (fast_tac (AC_cs addSIs [lam_type, RepFunI] addSEs [apply_type]) 1);
+by (fast_tac (AC_cs addSIs [lam_type] addSEs [apply_type]) 1);
 qed "AC1_AC4";
 
 
@@ -87,18 +87,18 @@
 (* ********************************************************************** *)
 
 goal thy "!!f. f:A->B ==> (UN z:A. {z}*f`z) <= A*Union(B)";
-by (fast_tac (ZF_cs addSDs [apply_type] addSEs [UN_E, singletonE]) 1);
+by (fast_tac (ZF_cs addSDs [apply_type]) 1);
 val lemma1 = result();
 
 goal thy "!!f. domain(UN z:A. {z}*f(z)) = {a:A. f(a)~=0}";
 by (fast_tac (ZF_cs addIs [equalityI]
                 addSEs [not_emptyE]
-                addSIs [singletonI, not_emptyI]
+                addSIs [not_emptyI]
                 addDs [range_type]) 1);
 val lemma2 = result();
 
 goal thy "!!f. x:A ==> (UN z:A. {z}*f(z))``{x} = f(x)";
-by (fast_tac (ZF_cs addIs [equalityI] addSIs [singletonI, UN_I] addSEs [singletonE, UN_E]) 1);
+by (fast_tac (ZF_cs addIs [equalityI]) 1);
 val lemma3 = result();
 
 goalw thy AC_defs "!!Z. AC4 ==> AC3";

--- a/src/ZF/AC/DC.ML	Mon Aug 19 15:35:11 1996 +0200
+++ b/src/ZF/AC/DC.ML	Tue Aug 20 12:23:13 1996 +0200
@@ -54,7 +54,7 @@
 by (fast_tac (AC_cs addSIs [nat_1I RS UN_I, singleton_fun RS Pi_type]
         addss (AC_ss addsimps [[lepoll_refl, succI1] MRS lepoll_1_is_sing,
         apply_singleton_eq, image_0])) 1);
-by (asm_full_simp_tac (AC_ss addsimps [domain_0, restrict_0, domain_sing,
+by (asm_full_simp_tac (AC_ss addsimps [domain_0, restrict_0, domain_cons,
                 [lepoll_refl, succI1] MRS lepoll_1_is_sing]) 1);
 val lemma1_2 = result();
 
@@ -192,8 +192,8 @@
 by (fast_tac (AC_cs addSEs [nat_succI]) 1);
 by (dresolve_tac [nat_succI RSN (4, lemma2)] 1
         THEN REPEAT (assume_tac 1));
-by (fast_tac (AC_cs addSEs [conjE, image_fun RS sym,
-        nat_into_Ord RSN (2, OrdmemD)]) 1);
+by (fast_tac (AC_cs addSEs [nat_into_Ord RSN (2, OrdmemD) RSN 
+			    (2, image_fun RS sym)]) 1);
 val lemma3 = result();
 
 goal thy "!!f. [| f:A->B; B<=C |] ==> f:A->C";

--- a/src/ZF/AC/DC_lemmas.ML	Mon Aug 19 15:35:11 1996 +0200
+++ b/src/ZF/AC/DC_lemmas.ML	Tue Aug 20 12:23:13 1996 +0200
@@ -50,10 +50,6 @@
 by (fast_tac AC_cs 1);
 val range_subset_domain = result();
 
-goal thy "domain({<x,y>}) = {x}";
-by (fast_tac (AC_cs addSIs [equalityI, singletonI] addSEs [singletonE]) 1);
-val domain_sing = result();
-
 val prems = goal thy "!!k. k:n ==> k~=n";
 by (fast_tac (AC_cs addSEs [mem_irrefl]) 1);
 val mem_not_eq = result();

--- a/src/ZF/AC/WO1_WO8.ML	Mon Aug 19 15:35:11 1996 +0200
+++ b/src/ZF/AC/WO1_WO8.ML	Tue Aug 20 12:23:13 1996 +0200
@@ -25,6 +25,6 @@
                         well_ord_rvimage]) 2);
 by (res_inst_tac [("x","lam a:{{x}. x:A}. THE x. a={x}")] exI 1);
 by (fast_tac (ZF_cs addSEs [RepFunE, singleton_eq_iff RS iffD1 RS sym]
-                addSIs [lam_type, singletonI]
+                addSIs [lam_type]
                 addIs [the_equality RS ssubst]) 1);
 qed "WO8_WO1";

--- a/src/ZF/AC/WO2_AC16.ML	Mon Aug 19 15:35:11 1996 +0200
+++ b/src/ZF/AC/WO2_AC16.ML	Tue Aug 20 12:23:13 1996 +0200
@@ -126,8 +126,7 @@
 val Finite_lesspoll_infinite_Ord = result();
 
 goal thy "!!x. x:X ==> Union(X) = Union(X-{x}) Un x";
-by (fast_tac (AC_cs addIs [equalityI] addSIs [singletonI]
-                addSEs [singletonE]) 1);
+by (fast_tac eq_cs 1);
 val Union_eq_Un_Diff = result();
 
 goal thy "!!n. n:nat ==> ALL X. X eqpoll n --> (ALL x:X. Finite(x))  \
@@ -185,8 +184,7 @@
 (* ********************************************************************** *)
 
 goal thy "A Un {a} = cons(a, A)";
-by (fast_tac (AC_cs addSIs [singletonI]
-                addSEs [singletonE] addIs [equalityI]) 1);
+by (fast_tac eq_cs 1);
 val Un_sing_eq_cons = result();
 
 goal thy "!!A. A lepoll B ==> A Un {a} lepoll succ(B)";
@@ -236,7 +234,7 @@
 val Least_eq_imp_ex = result();
 
 goal thy "!!A. [| A lepoll 1; a:A; b:A |] ==> a=b";
-by (fast_tac (AC_cs addSDs [lepoll_1_is_sing] addSEs [singletonE]) 1);
+by (fast_tac (AC_cs addSDs [lepoll_1_is_sing]) 1);
 val two_in_lepoll_1 = result();
 
 goal thy "!!a. [| ALL i<a. F(i)-(UN j<i. F(j)) lepoll 1; Limit(a) |]  \
@@ -366,8 +364,7 @@
 (* ********************************************************************** *)
 
 goal thy "!!A. [| A <= B; a : A; A - {a} = B - {a} |] ==> A = B";
-by (fast_tac (AC_cs addSEs [equalityE, singletonE]
-                addSIs [equalityI, singletonI]) 1);
+by (fast_tac (eq_cs addSEs [equalityE]) 1);
 val Diffs_eq_imp_eq = result();
 
 goal thy "!!A. m:nat ==> ALL A B. A <= B & m lepoll A & B lepoll m --> A=B";
@@ -383,7 +380,7 @@
 by (REPEAT (eresolve_tac [allE, impE] 1));
 by (rtac conjI 1);
 by (fast_tac AC_cs 2);
-by (fast_tac (AC_cs addSEs [singletonE] addSIs [singletonI]) 1);
+by (fast_tac (eq_cs addSEs [singletonE]) 1);
 by (etac Diffs_eq_imp_eq 1
         THEN REPEAT (assume_tac 1));
 val subset_imp_eq_lemma = result();
@@ -459,7 +456,7 @@
 val ex_next_Ord = result();
 
 goal thy "!!Z. [| EX! Y. Y:Z & P(Y); ~P(W) |] ==> EX! Y. Y:Z Un {W} & P(Y)";
-by (fast_tac (AC_cs addSEs [singletonE]) 1);
+by (fast_tac ZF_cs 1);
 val ex1_in_Un_sing = result();
 
 (* ********************************************************************** *)

--- a/src/ZF/AC/rel_is_fun.ML	Mon Aug 19 15:35:11 1996 +0200
+++ b/src/ZF/AC/rel_is_fun.ML	Tue Aug 20 12:23:13 1996 +0200
@@ -29,7 +29,7 @@
 by (fast_tac (ZF_cs addSIs [domain_mono]) 1);
 by (rtac subsetI 1);
 by (excluded_middle_tac "x = a" 1);
-by (REPEAT (fast_tac (ZF_cs addSIs [domainI] addSEs [domainE]) 1));
+by (REPEAT (fast_tac ZF_cs 1));
 val domain_Diff_eq_domain = result();
 
 goalw Cardinal.thy [function_def]