# HG changeset patch
# User paulson
# Date 840620617 -7200
# Node ID cc9f1ba8f29a06c96853957b27f00e7807551f40
# Parent  c77409a88b75b697f86eb75467c9c7a62cd61e8b
Tidying: removing redundant args in classical reasoner calls

diff -r c77409a88b75 -r cc9f1ba8f29a src/ZF/AC/AC10_AC15.ML
--- a/src/ZF/AC/AC10_AC15.ML	Wed Aug 21 11:00:04 1996 +0200
+++ b/src/ZF/AC/AC10_AC15.ML	Wed Aug 21 11:43:37 1996 +0200
@@ -190,7 +190,7 @@
 by (asm_full_simp_tac (AC_ss addsimps
                 [singleton_eqpoll_1 RS eqpoll_imp_lepoll,
                 singletonI RS not_emptyI]) 1);
-by (fast_tac (AC_cs addSEs [singletonE, apply_type]) 1);
+by (fast_tac (AC_cs addSEs [apply_type]) 1);
 qed "AC1_AC13";
 
 (* ********************************************************************** *)
diff -r c77409a88b75 -r cc9f1ba8f29a src/ZF/AC/AC16_WO4.ML
--- a/src/ZF/AC/AC16_WO4.ML	Wed Aug 21 11:00:04 1996 +0200
+++ b/src/ZF/AC/AC16_WO4.ML	Wed Aug 21 11:43:37 1996 +0200
@@ -24,7 +24,7 @@
 by (fast_tac (AC_cs addSIs [ltI, nat_into_Ord, lam_funtype RS domain_of_fun,
         equalityI, singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans,
         nat_1_lepoll_iff RS iffD2]
-        addSEs [singletonE, apply_type, ltE]) 1);
+        addSEs [apply_type, ltE]) 1);
 val lemma1 = result();
 
 (* ********************************************************************** *)
diff -r c77409a88b75 -r cc9f1ba8f29a src/ZF/AC/AC2_AC6.ML
--- a/src/ZF/AC/AC2_AC6.ML	Wed Aug 21 11:00:04 1996 +0200
+++ b/src/ZF/AC/AC2_AC6.ML	Wed Aug 21 11:43:37 1996 +0200
@@ -16,7 +16,7 @@
 
 goal thy "!!B. [| B:A; f:(PROD X:A. X); 0~:A |]  \
 \               ==> {f`B} <= B Int {f`C. C:A}";
-by (fast_tac (AC_cs addSEs [singletonE, apply_type, RepFunI]) 1);
+by (fast_tac (ZF_cs addSEs [apply_type]) 1);
 val lemma1 = result();
 
 goalw thy [pairwise_disjoint_def]
@@ -143,7 +143,7 @@
 by (rtac apply_equality 1 THEN (assume_tac 2));
 by (etac domainE 1);
 by (forward_tac [range_type] 1 THEN (assume_tac 1));
-by (fast_tac (ZF_cs addSEs [singletonE, converseD] addDs [apply_equality]) 1);
+by (fast_tac (ZF_cs addDs [apply_equality]) 1);
 qed "AC4_AC5";
 
 
@@ -157,9 +157,9 @@
 
 goalw thy [range_def] "!!A. R <= A*B ==> range(lam x:R. fst(x)) = domain(R)";
 by (rtac equalityI 1);
-by (fast_tac (AC_cs addSEs [lamE, Pair_inject]
+by (fast_tac (AC_cs addSEs [lamE]
                 addEs [subst_elem]
-                addSDs [converseD, Pair_fst_snd_eq]) 1);
+                addSDs [Pair_fst_snd_eq]) 1);
 by (rtac subsetI 1);
 by (etac domainE 1);
 by (rtac domainI 1);
diff -r c77409a88b75 -r cc9f1ba8f29a src/ZF/AC/Cardinal_aux.ML
--- a/src/ZF/AC/Cardinal_aux.ML	Wed Aug 21 11:00:04 1996 +0200
+++ b/src/ZF/AC/Cardinal_aux.ML	Wed Aug 21 11:43:37 1996 +0200
@@ -76,7 +76,7 @@
 by (split_tac [expand_if] 1);
 by (asm_full_simp_tac (ZF_ss addsimps [double_Diff_sing, Diff_eq_0_iff]) 1);
 by (fast_tac (ZF_cs addSIs [the_equality, equalityI, equals0I]
-                addEs [equalityE] addSEs [singletonE]) 1);
+                addEs [equalityE]) 1);
 val paired_bij_lemma = result();
 
 goal thy "(lam y:{{y,z}. y:x}. if(y-{z}=0, z, THE w. y-{z}={w}))  \
@@ -131,7 +131,7 @@
 by (res_inst_tac [("x","lam z:(UN x:a. {P(x)}). (LEAST i. P(i)=z)")] exI 1);
 by (res_inst_tac [("d","%z. P(z)")] lam_injective 1);
 by (fast_tac (AC_cs addSIs [Least_in_Ord]) 1);
-by (fast_tac (AC_cs addIs [LeastI] addSEs [singletonE, Ord_in_Ord]) 1);
+by (fast_tac (AC_cs addIs [LeastI] addSEs [Ord_in_Ord]) 1);
 val UN_sing_lepoll = result();
 
 goal thy "!!a T. [| well_ord(T, R); ~Finite(a); Ord(a); n:nat |] ==>  \
diff -r c77409a88b75 -r cc9f1ba8f29a src/ZF/AC/DC.ML
--- a/src/ZF/AC/DC.ML	Wed Aug 21 11:00:04 1996 +0200
+++ b/src/ZF/AC/DC.ML	Wed Aug 21 11:43:37 1996 +0200
@@ -302,8 +302,7 @@
 \       |] ==> RR <= Pow(XX)*XX &  \
 \       (ALL Y:Pow(XX). Y lesspoll nat --> (EX x:XX. <Y,x>:RR))";
 by (rtac conjI 1);
-by (fast_tac (FOL_cs addSEs [FinD RS PowI, SigmaE, CollectE]
-        addSIs [subsetI, SigmaI]) 1);
+by (deepen_tac (ZF_cs addSEs [FinD RS PowI]) 0 1);
 by (rtac ballI 1);
 by (rtac impI 1);
 by (dresolve_tac [[lesspoll_nat_is_Finite, PowD] MRS Finite_Fin] 1
diff -r c77409a88b75 -r cc9f1ba8f29a src/ZF/AC/WO1_WO6.ML
--- a/src/ZF/AC/WO1_WO6.ML	Wed Aug 21 11:00:04 1996 +0200
+++ b/src/ZF/AC/WO1_WO6.ML	Wed Aug 21 11:43:37 1996 +0200
@@ -33,11 +33,11 @@
 (* ********************************************************************** *)
 
 goal thy "!!f. f: A->B ==> (lam x:A. {f`x}): A -> {{b}. b:B}";
-by (fast_tac (ZF_cs addSIs [lam_type, RepFunI, apply_type]) 1);
+by (fast_tac (ZF_cs addSIs [lam_type, apply_type]) 1);
 val lam_sets = result();
 
 goalw thy [surj_def] "!!f. f:surj(A,B) ==> (UN a:A. {f`a}) = B";
-by (fast_tac (ZF_cs addSIs [equalityI] addSEs [singletonE, apply_type]) 1);
+by (fast_tac (ZF_cs addSIs [equalityI] addSEs [apply_type]) 1);
 val surj_imp_eq_ = result();
 
 goal thy "!!f. [| f:surj(A,B); Ord(A) |] ==> (UN a<A. {f`a}) = B";
diff -r c77409a88b75 -r cc9f1ba8f29a src/ZF/AC/WO1_WO8.ML
--- a/src/ZF/AC/WO1_WO8.ML	Wed Aug 21 11:00:04 1996 +0200
+++ b/src/ZF/AC/WO1_WO8.ML	Wed Aug 21 11:43:37 1996 +0200
@@ -24,7 +24,7 @@
 by (fast_tac (AC_cs addSEs [lam_sing_bij RS bij_is_inj RS
                         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]
+by (fast_tac (ZF_cs addSEs [singleton_eq_iff RS iffD1 RS sym]
                 addSIs [lam_type]
                 addIs [the_equality RS ssubst]) 1);
 qed "WO8_WO1";
diff -r c77409a88b75 -r cc9f1ba8f29a src/ZF/AC/WO2_AC16.ML
--- a/src/ZF/AC/WO2_AC16.ML	Wed Aug 21 11:00:04 1996 +0200
+++ b/src/ZF/AC/WO2_AC16.ML	Wed Aug 21 11:43:37 1996 +0200
@@ -380,7 +380,7 @@
 by (REPEAT (eresolve_tac [allE, impE] 1));
 by (rtac conjI 1);
 by (fast_tac AC_cs 2);
-by (fast_tac (eq_cs addSEs [singletonE]) 1);
+by (fast_tac ZF_cs 1);
 by (etac Diffs_eq_imp_eq 1
         THEN REPEAT (assume_tac 1));
 val subset_imp_eq_lemma = result();