# HG changeset patch
# User paulson
# Date 852801603 -3600
# Node ID 40efb87985b50fcf78e725e0c740b815e13a05a6
# Parent  82ec47e0a8d3538c036ad616dc230747c51d61f5
Removal of needless "addIs [equality]", etc.

diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/AC/AC15_WO6.ML
--- a/src/ZF/AC/AC15_WO6.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/AC15_WO6.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -8,7 +8,7 @@
 open AC15_WO6;
 
 goal thy "!!x. Ord(x) ==> (UN a<x. F(a)) = (UN a:x. F(a))";
-by (fast_tac (!claset addSIs [equalityI, ltI] addSDs [ltD]) 1);
+by (fast_tac (!claset addSIs [ltI] addSDs [ltD]) 1);
 val OUN_eq_UN = result();
 
 val [prem] = goal thy "ALL x:Pow(A)-{0}. f`x~=0 & f`x<=x & f`x lepoll m ==>  \
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/AC/AC16_WO4.ML
--- a/src/ZF/AC/AC16_WO4.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/AC16_WO4.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -297,7 +297,7 @@
 by (asm_full_simp_tac (!simpset addsimps [add_succ]) 1);
 by (fast_tac (!claset addSIs [Diff_sing_eqpoll, lepoll_Diff_sing]) 1);
 by (res_inst_tac [("P","%z. z lepoll m")] subst 1 THEN (assume_tac 2));
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
 val eqpoll_sum_imp_Diff_lepoll_lemma = result();
 
 goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) lepoll B;  \
@@ -329,7 +329,7 @@
         eqpoll_sym RSN (2, Diff_sing_eqpoll) RS eqpoll_sym]
         addss (!simpset addsimps [add_succ])) 1);
 by (res_inst_tac [("P","%z. z eqpoll m")] subst 1 THEN (assume_tac 2));
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
 val eqpoll_sum_imp_Diff_eqpoll_lemma = result();
 
 goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) eqpoll B;  \
@@ -347,7 +347,7 @@
 
 goal thy "!!w. [| x Int y = 0; w <= x Un y |]  \
 \        ==> w Int (x - {u}) = w - cons(u, w Int y)";
-by (fast_tac (!claset addSIs [equalityI] addEs [equals0D]) 1);
+by (fast_tac (!claset addEs [equals0D]) 1);
 val w_Int_eq_w_Diff = result();
 
 goal thy "!!w. [| w:{v:s_u(u, t_n, succ(l), y). a <= v};  \
@@ -440,7 +440,7 @@
 
 goal thy "{x:Pow(X). x lepoll 0} = {0}";
 by (fast_tac (!claset addSDs [lepoll_0_is_0]
-                    addSIs [lepoll_refl, equalityI]) 1);
+                      addSIs [lepoll_refl]) 1);
 val subsets_lepoll_0_eq_unit = result();
 
 goal thy "!!X. [| well_ord(X, R); ~Finite(X); n:nat |]  \
@@ -453,8 +453,7 @@
 
 goal thy "!!n. n:nat ==> {z:Pow(y). z lepoll succ(n)} =  \
 \       {z:Pow(y). z lepoll n} Un {z:Pow(y). z eqpoll succ(n)}";
-by (fast_tac (!claset addIs [le_refl, leI,
-                le_imp_lepoll, equalityI]
+by (fast_tac (!claset addIs [le_refl, leI, le_imp_lepoll]
                 addSDs [lepoll_succ_disj]
                 addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1);
 val subsets_lepoll_succ = result();
@@ -476,7 +475,7 @@
 val tot_ord_unit = result();
 
 goalw thy [wf_on_def, wf_def] "wf[{a}](0)";
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
 val wf_on_unit = result();
 
 goalw thy [well_ord_def] "well_ord({a},0)";
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/AC/AC16_lemmas.ML
--- a/src/ZF/AC/AC16_lemmas.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/AC16_lemmas.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -8,7 +8,7 @@
 open AC16_lemmas;
 
 goal thy "!!a. a~:A ==> cons(a,A)-{a}=A";
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
 val cons_Diff_eq = result();
 
 goalw thy [lepoll_def] "1 lepoll X <-> (EX x. x:X)";
@@ -94,7 +94,7 @@
 val prems = goal thy "(!!y. y:z ==> Ord(y)) ==> z <= succ(Union(z))";
 by (rtac subsetI 1);
 by (res_inst_tac [("Q","ALL y:z. y<=x")] (excluded_middle RS disjE) 1);
-by (fast_tac (!claset addSIs [equalityI]) 2);
+by (Fast_tac 2);
 by (etac swap 1);
 by (rtac ballI 1);
 by (rtac Ord_linear_le 1);
@@ -114,16 +114,15 @@
 val succ_Union_not_mem = result();
 
 goal thy "Union(cons(succ(Union(z)),z)) = succ(Union(z))";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 val Union_cons_eq_succ_Union = result();
 
 goal thy "!!i. [| Ord(i); Ord(j) |] ==> i Un j = i | i Un j = j";
-by (fast_tac (!claset addSDs [le_imp_subset] addIs [equalityI]
-                addEs [Ord_linear_le]) 1);
+by (fast_tac (!claset addSDs [le_imp_subset] addEs [Ord_linear_le]) 1);
 val Un_Ord_disj = result();
 
 goal thy "!!X. x:X ==> Union(X) = x Un Union(X-{x})";
-by (fast_tac (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 val Union_eq_Un = result();
 
 goal thy "!!n. n:nat ==>  \
@@ -208,12 +207,12 @@
 
 goalw thy [surj_def] "!!f. [| f:surj(A,B); y<=B |]  \
 \       ==> f``(converse(f)``y) = y";
-by (fast_tac (!claset addSIs [equalityI] addDs [apply_equality2]
-        addEs [apply_iff RS iffD2]) 1);
+by (fast_tac (!claset addDs [apply_equality2]
+	              addEs [apply_iff RS iffD2]) 1);
 val image_vimage_eq = result();
 
 goal thy "!!f. [| f:inj(A,B); y<=A |] ==> converse(f)``(f``y) = y";
-by (fast_tac (!claset addSIs [equalityI] addSEs [inj_is_fun RS apply_Pair]
+by (fast_tac (!claset addSEs [inj_is_fun RS apply_Pair]
                 addDs [inj_equality]) 1);
 val vimage_image_eq = result();
 
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/AC/AC17_AC1.ML
--- a/src/ZF/AC/AC17_AC1.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/AC17_AC1.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -56,8 +56,7 @@
 goal thy "!!x. ~ (EX f: Pow(x)-{0}->x. x - F(f) = 0)  \
 \       ==> (lam f: Pow(x)-{0}->x. x - F(f))  \
 \               : (Pow(x) -{0} -> x) -> Pow(x) - {0}";
-by (fast_tac (!claset addSIs [lam_type] addIs [equalityI]
-                addSDs [Diff_eq_0_iff RS iffD1]) 1);
+by (fast_tac (!claset addSIs [lam_type] addSDs [Diff_eq_0_iff RS iffD1]) 1);
 val lemma2 = result();
 
 goal thy "!!f. [| f`Z : Z; Z:Pow(x)-{0} |] ==>  \
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/AC/AC18_AC19.ML
--- a/src/ZF/AC/AC18_AC19.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/AC18_AC19.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -37,7 +37,7 @@
 
 val [prem] = goalw thy (AC18_def::AC_defs) "AC1 ==> AC18";
 by (resolve_tac [prem RS revcut_rl] 1);
-by (fast_tac (!claset addSEs [lemma_AC18, UN_E, not_emptyE, apply_type]
+by (fast_tac (!claset addSEs [lemma_AC18, not_emptyE, apply_type]
                 addSIs [equalityI, INT_I, UN_I]) 1);
 qed "AC1_AC18";
 
@@ -70,7 +70,7 @@
 by (rtac subsetI 1);
 by (excluded_middle_tac "x=0" 1);
 by (Fast_tac 1);
-by (fast_tac (!claset addEs [notE, subst_elem] addSIs [equalityI])  1);
+by (fast_tac (!claset addEs [notE, subst_elem])  1);
 val lemma1_1 = result();
 
 goalw thy [u_def]
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/AC/AC2_AC6.ML
--- a/src/ZF/AC/AC2_AC6.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/AC2_AC6.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -91,14 +91,11 @@
 val lemma1 = result();
 
 goal thy "!!f. domain(UN z:A. {z}*f(z)) = {a:A. f(a)~=0}";
-by (fast_tac (!claset addIs [equalityI]
-                addSEs [not_emptyE]
-                addSIs [not_emptyI]
-                addDs [range_type]) 1);
+by (fast_tac (!claset 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 (!claset addIs [equalityI]) 1);
+by (Fast_tac 1);
 val lemma3 = result();
 
 goalw thy AC_defs "!!Z. AC4 ==> AC3";
@@ -116,7 +113,7 @@
 goal thy "!!A. b~:A ==> (PROD x:{a:A. id(A)`a~=b}. id(A)`x) = (PROD x:A. x)";
 by (asm_full_simp_tac (!simpset addsimps [id_def] addcongs [Pi_cong]) 1);
 by (res_inst_tac [("b","A")] subst_context 1);
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
 val lemma = result();
 
 goalw thy AC_defs "!!Z. AC3 ==> AC1";
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/AC/AC_Equiv.ML
--- a/src/ZF/AC/AC_Equiv.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/AC_Equiv.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -150,9 +150,9 @@
 
 goalw thy [surj_def] "!!f. f : surj(A, B) ==> f``A = B";
 by (etac CollectE 1);
-by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1 THEN (assume_tac 1));
-by (fast_tac (!claset addSEs [RepFunE, apply_type]
-                addSIs [RepFunI] addIs [equalityI]) 1);
+by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1 
+    THEN (assume_tac 1));
+by (fast_tac (!claset addSEs [apply_type] addIs [equalityI]) 1);
 val surj_image_eq = result();
 
 
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/AC/Cardinal_aux.ML
--- a/src/ZF/AC/Cardinal_aux.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/Cardinal_aux.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -75,8 +75,7 @@
 goal upair.thy "if({y,z}-{z}=0, z, THE w. {y,z}-{z}={w}) = y";
 by (split_tac [expand_if] 1);
 by (asm_full_simp_tac (!simpset addsimps [double_Diff_sing, Diff_eq_0_iff]) 1);
-by (fast_tac (!claset addSIs [the_equality, equalityI, equals0I]
-                addEs [equalityE]) 1);
+by (fast_tac (!claset addSIs [the_equality] 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}))  \
@@ -120,7 +119,7 @@
 by (fast_tac (!claset addSIs [Diff_sing_lepoll, the_first_in]) 1);
 by (res_inst_tac [("b","y-{THE b. first(b, y, r)}")] subst 1);
 by (rtac empty_lepollI 2);
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
 val Diff_first_lepoll = result();
 
 goal thy "(UN x:X. P(x)) <= (UN x:X. P(x)-Q(x)) Un (UN x:X. Q(x))";
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/AC/DC.ML
--- a/src/ZF/AC/DC.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/DC.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -316,7 +316,7 @@
 goal thy "!!f. [| (UN x:f``n. P(x)) = y; P(f`n) = succ(y);  \
 \       f:nat -> X; n:nat |] ==> (UN x:f``succ(n). P(x)) = succ(y)";
 by (asm_full_simp_tac (!simpset addsimps [UN_image_succ_eq]) 1);
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
 val UN_image_succ_eq_succ = result();
 
 goal thy "!!f. [| f:succ(n) -> D;  n:nat;  \
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/AC/DC_lemmas.ML
--- a/src/ZF/AC/DC_lemmas.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/DC_lemmas.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -55,7 +55,7 @@
 val cons_fun_type2 = result();
 
 goal thy "!!n. n: nat ==> cons(<n,x>, g)``n = g``n";
-by (fast_tac (!claset addSIs [equalityI] addSEs [mem_irrefl]) 1);
+by (fast_tac (!claset addSEs [mem_irrefl]) 1);
 val cons_image_n = result();
 
 goal thy "!!n. g:n->X ==> cons(<n,x>, g)`n = x";
@@ -63,7 +63,7 @@
 val cons_val_n = result();
 
 goal thy "!!k. k : n ==> cons(<n,x>, g)``k = g``k";
-by (fast_tac (!claset addSIs [equalityI] addEs [mem_asym]) 1);
+by (fast_tac (!claset addEs [mem_asym]) 1);
 val cons_image_k = result();
 
 goal thy "!!k. [| k:n; g:n->X |] ==> cons(<n,x>, g)`k = g`k";
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/AC/HH.ML
--- a/src/ZF/AC/HH.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/HH.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -29,7 +29,7 @@
 val HH_values = result();
 
 goal thy "!!A. B<=A ==> X-(UN a:A. P(a)) = X-(UN a:A-B. P(a))-(UN b:B. P(b))";
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
 val subset_imp_Diff_eq = result();
 
 goal thy "!!c. [| c:a-b; b<a |] ==> c=b | b<c & c<a";
@@ -41,8 +41,7 @@
 
 val prems = goal thy "(!!y. y:A ==> P(y) = {x}) ==> x - (UN y:A. P(y)) = x";
 by (asm_full_simp_tac (!simpset addsimps prems) 1);
-by (fast_tac (!claset addSIs [equalityI] addSDs [prem]
-                addSEs [RepFunE, mem_irrefl]) 1);
+by (fast_tac (!claset addSDs [prem] addSEs [mem_irrefl]) 1);
 val Diff_UN_eq_self = result();
 
 goal thy "!!a. x - (UN b:a. HH(f,x,b)) = x - (UN b:a1. HH(f,x,b))  \
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/AC/WO1_AC.ML
--- a/src/ZF/AC/WO1_AC.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/WO1_AC.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -101,8 +101,7 @@
 
 goalw thy [bij_def, surj_def]
         "!!f. f : bij(D+D, B) ==> Union({{f`Inl(i), f`Inr(i)}. i:D})=B";
-by (fast_tac (!claset addSEs [inj_is_fun RS apply_type, CollectE, sumE]
-        addSIs [InlI, InrI, equalityI]) 1);
+by (fast_tac (!claset addSEs [inj_is_fun RS apply_type]) 1);
 val lemma2_5 = result();
 
 goal thy "!!A. [| WO1; ~Finite(B); 1 le n  |]  \
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/AC/WO1_WO6.ML
--- a/src/ZF/AC/WO1_WO6.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/WO1_WO6.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -37,12 +37,12 @@
 val lam_sets = result();
 
 goalw thy [surj_def] "!!f. f:surj(A,B) ==> (UN a:A. {f`a}) = B";
-by (fast_tac (!claset addSIs [equalityI] addSEs [apply_type]) 1);
+by (fast_tac (!claset addSEs [apply_type]) 1);
 val surj_imp_eq_ = result();
 
 goal thy "!!f. [| f:surj(A,B); Ord(A) |] ==> (UN a<A. {f`a}) = B";
 by (fast_tac (!claset addSDs [surj_imp_eq_]
-                addSIs [equalityI, ltI] addSEs [ltE]) 1);
+                addSIs [ltI] addSEs [ltE]) 1);
 val surj_imp_eq = result();
 
 goalw thy WO_defs "!!Z. WO1 ==> WO4(1)";
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/AC/WO2_AC16.ML
--- a/src/ZF/AC/WO2_AC16.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/AC/WO2_AC16.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -191,7 +191,7 @@
 val Un_lepoll_succ = result();
 
 goal thy "!!a. Ord(a) ==> F(a) - (UN b<succ(a). F(b)) = 0";
-by (fast_tac (!claset addSIs [OUN_I, le_refl] addIs [equalityI]) 1);
+by (fast_tac (!claset addSIs [OUN_I, le_refl]) 1);
 val Diff_UN_succ_empty = result();
 
 goal thy "!!a. Ord(a) ==> F(a) Un X - (UN b<succ(a). F(b)) <= X";
@@ -366,7 +366,7 @@
 
 goal thy "!!A. m:nat ==> ALL A B. A <= B & m lepoll A & B lepoll m --> A=B";
 by (etac nat_induct 1);
-by (fast_tac (!claset addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
+by (fast_tac (!claset addSDs [lepoll_0_is_0]) 1);
 by (REPEAT (resolve_tac [allI, impI] 1));
 by (REPEAT (etac conjE 1));
 by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/Epsilon.ML
--- a/src/ZF/Epsilon.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/Epsilon.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -228,7 +228,7 @@
 
 goal Epsilon.thy "rank(0) = 0";
 by (rtac (rank RS trans) 1);
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (Fast_tac 1);
 qed "rank_0";
 
 goal Epsilon.thy "rank(succ(x)) = succ(rank(x))";
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/EquivClass.ML
--- a/src/ZF/EquivClass.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/EquivClass.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -26,8 +26,7 @@
 
 goalw EquivClass.thy [equiv_def]
     "!!A r. equiv(A,r) ==> converse(r) O r = r";
-by (fast_tac (subset_cs addSIs [equalityI, sym_trans_comp_subset, 
-                                refl_comp_subset]) 1);
+by (fast_tac (subset_cs addSIs [sym_trans_comp_subset, refl_comp_subset]) 1);
 qed "equiv_comp_eq";
 
 (*second half*)
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/IMP/Equiv.ML
--- a/src/ZF/IMP/Equiv.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/IMP/Equiv.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -120,7 +120,7 @@
 
 goal Equiv.thy
     "ALL c:com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}";
-by (fast_tac (!claset addIs [equalityI, C_subset RS subsetD]
+by (fast_tac (!claset addIs [C_subset RS subsetD]
 	              addEs [com2 RS bspec]
 		      addDs [com1]
 		      addss (!simpset)) 1);
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/List.ML
--- a/src/ZF/List.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/List.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -28,8 +28,7 @@
 
 goal List.thy "list(A) = {0} + (A * list(A))";
 let open list;  val rew = rewrite_rule con_defs in  
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
-                     addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
 end;
 qed "list_unfold";
 
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/ex/Brouwer.ML
--- a/src/ZF/ex/Brouwer.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/ex/Brouwer.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -14,8 +14,7 @@
 
 goal Brouwer.thy "brouwer = {0} + brouwer + (nat -> brouwer)";
 let open brouwer;  val rew = rewrite_rule con_defs in  
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
-                     addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
 end;
 qed "brouwer_unfold";
 
@@ -38,8 +37,7 @@
 
 goal Brouwer.thy "Well(A,B) = (SUM x:A. B(x) -> Well(A,B))";
 let open Well;  val rew = rewrite_rule con_defs in  
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
-                     addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
 end;
 qed "Well_unfold";
 
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/ex/Comb.ML
--- a/src/ZF/ex/Comb.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/ex/Comb.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -29,7 +29,7 @@
 val contract_combD2 = contract.dom_subset RS subsetD RS SigmaD2;
 
 goal Comb.thy "field(contract) = comb";
-by (fast_tac (!claset addIs [equalityI,contract.K] addSEs [contract_combE2]) 1);
+by (fast_tac (!claset addIs [contract.K] addSEs [contract_combE2]) 1);
 qed "field_contract_eq";
 
 bind_thm ("reduction_refl",
@@ -121,8 +121,8 @@
 val parcontract_combD2 = parcontract.dom_subset RS subsetD RS SigmaD2;
 
 goal Comb.thy "field(parcontract) = comb";
-by (fast_tac (!claset addIs [equalityI, parcontract.K] 
-                    addSEs [parcontract_combE2]) 1);
+by (fast_tac (!claset addIs [parcontract.K] 
+                      addSEs [parcontract_combE2]) 1);
 qed "field_parcontract_eq";
 
 (*Derive a case for each combinator constructor*)
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/ex/Data.ML
--- a/src/ZF/ex/Data.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/ex/Data.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -11,8 +11,7 @@
 
 goal Data.thy "data(A,B) = ({0} + A) + (A*B + A*B*data(A,B))";
 let open data;  val rew = rewrite_rule con_defs in  
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
-                     addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
 end;
 qed "data_unfold";
 
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/ex/LList.ML
--- a/src/ZF/ex/LList.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/ex/LList.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -23,8 +23,7 @@
 
 goal LList.thy "llist(A) = {0} <+> (A <*> llist(A))";
 let open llist;  val rew = rewrite_rule con_defs in  
-by (fast_tac (!claset addSIs (subsetI :: equalityI :: map rew intrs)
-                      addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (subsetI ::map rew intrs) addEs [rew elim]) 1)
 end;
 qed "llist_unfold";
 
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/ex/Ntree.ML
--- a/src/ZF/ex/Ntree.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/ex/Ntree.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -15,8 +15,7 @@
 
 goal Ntree.thy "ntree(A) = A * (UN n: nat. n -> ntree(A))";
 let open ntree;  val rew = rewrite_rule con_defs in  
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
-                     addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
 end;
 qed "ntree_unfold";
 
@@ -70,8 +69,7 @@
 
 goal Ntree.thy "maptree(A) = A * (maptree(A) -||> maptree(A))";
 let open maptree;  val rew = rewrite_rule con_defs in  
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
-                     addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
 end;
 qed "maptree_unfold";
 
@@ -95,8 +93,7 @@
 
 goal Ntree.thy "maptree2(A,B) = A * (B -||> maptree2(A,B))";
 let open maptree2;  val rew = rewrite_rule con_defs in  
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
-                     addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
 end;
 qed "maptree2_unfold";
 
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/ex/TF.ML
--- a/src/ZF/ex/TF.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/ex/TF.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -38,8 +38,7 @@
     "tree_forest(A) = (A*forest(A)) + ({0} + tree(A)*forest(A))";
 let open tree_forest;  
     val rew = rewrite_rule (con_defs @ tl defs) in  
-by (fast_tac (!claset addSIs (equalityI :: (map rew intrs RL [PartD1]))
-                     addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs RL [PartD1]) addEs [rew elim]) 1)
 end;
 qed "tree_forest_unfold";
 
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/ex/Term.ML
--- a/src/ZF/ex/Term.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/ex/Term.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -11,8 +11,7 @@
 
 goal Term.thy "term(A) = A * list(term(A))";
 let open term;  val rew = rewrite_rule con_defs in  
-by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
-                     addEs [rew elim]) 1)
+by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
 end;
 qed "term_unfold";
 
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/ex/misc.ML
--- a/src/ZF/ex/misc.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/ex/misc.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -145,9 +145,7 @@
 \    : bij(Pow(A+B), Pow(A)*Pow(B))";
 by (res_inst_tac [("d", "%<X,Y>.{Inl(x).x:X} Un {Inr(y).y:Y}")] 
     lam_bijective 1);
-by (TRYALL (etac SigmaE));
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS (fast_tac (!claset addSIs [equalityI])));
+by (Auto_tac());
 val Pow_bij = result();
 
 writeln"Reached end of file.";
diff -r 82ec47e0a8d3 -r 40efb87985b5 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Wed Jan 08 15:17:25 1997 +0100
+++ b/src/ZF/simpdata.ML	Thu Jan 09 10:20:03 1997 +0100
@@ -11,8 +11,7 @@
 (*For proving rewrite rules*)
 fun prove_fun s = 
     (writeln s;  prove_goal thy s
-       (fn prems => [ (cut_facts_tac prems 1), 
-                      (fast_tac (!claset addSIs [equalityI]) 1) ]));
+       (fn prems => [ (cut_facts_tac prems 1), (Fast_tac 1) ]));
 
 (*Are all these really suitable?*)
 val ball_simps = map prove_fun