Removal of needless "addIs [equality]", etc.
authorpaulson
Thu Jan 09 10:20:03 1997 +0100 (1997-01-09 ago)
changeset 249640efb87985b5
parent 2495 82ec47e0a8d3
child 2497 47de509bdd55
Removal of needless "addIs [equality]", etc.
src/ZF/AC/AC15_WO6.ML
src/ZF/AC/AC16_WO4.ML
src/ZF/AC/AC16_lemmas.ML
src/ZF/AC/AC17_AC1.ML
src/ZF/AC/AC18_AC19.ML
src/ZF/AC/AC2_AC6.ML
src/ZF/AC/AC_Equiv.ML
src/ZF/AC/Cardinal_aux.ML
src/ZF/AC/DC.ML
src/ZF/AC/DC_lemmas.ML
src/ZF/AC/HH.ML
src/ZF/AC/WO1_AC.ML
src/ZF/AC/WO1_WO6.ML
src/ZF/AC/WO2_AC16.ML
src/ZF/Epsilon.ML
src/ZF/EquivClass.ML
src/ZF/IMP/Equiv.ML
src/ZF/List.ML
src/ZF/ex/Brouwer.ML
src/ZF/ex/Comb.ML
src/ZF/ex/Data.ML
src/ZF/ex/LList.ML
src/ZF/ex/Ntree.ML
src/ZF/ex/TF.ML
src/ZF/ex/Term.ML
src/ZF/ex/misc.ML
src/ZF/simpdata.ML
     1.1 --- a/src/ZF/AC/AC15_WO6.ML	Wed Jan 08 15:17:25 1997 +0100
     1.2 +++ b/src/ZF/AC/AC15_WO6.ML	Thu Jan 09 10:20:03 1997 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  open AC15_WO6;
     1.5  
     1.6  goal thy "!!x. Ord(x) ==> (UN a<x. F(a)) = (UN a:x. F(a))";
     1.7 -by (fast_tac (!claset addSIs [equalityI, ltI] addSDs [ltD]) 1);
     1.8 +by (fast_tac (!claset addSIs [ltI] addSDs [ltD]) 1);
     1.9  val OUN_eq_UN = result();
    1.10  
    1.11  val [prem] = goal thy "ALL x:Pow(A)-{0}. f`x~=0 & f`x<=x & f`x lepoll m ==>  \
     2.1 --- a/src/ZF/AC/AC16_WO4.ML	Wed Jan 08 15:17:25 1997 +0100
     2.2 +++ b/src/ZF/AC/AC16_WO4.ML	Thu Jan 09 10:20:03 1997 +0100
     2.3 @@ -297,7 +297,7 @@
     2.4  by (asm_full_simp_tac (!simpset addsimps [add_succ]) 1);
     2.5  by (fast_tac (!claset addSIs [Diff_sing_eqpoll, lepoll_Diff_sing]) 1);
     2.6  by (res_inst_tac [("P","%z. z lepoll m")] subst 1 THEN (assume_tac 2));
     2.7 -by (fast_tac (!claset addSIs [equalityI]) 1);
     2.8 +by (Fast_tac 1);
     2.9  val eqpoll_sum_imp_Diff_lepoll_lemma = result();
    2.10  
    2.11  goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) lepoll B;  \
    2.12 @@ -329,7 +329,7 @@
    2.13          eqpoll_sym RSN (2, Diff_sing_eqpoll) RS eqpoll_sym]
    2.14          addss (!simpset addsimps [add_succ])) 1);
    2.15  by (res_inst_tac [("P","%z. z eqpoll m")] subst 1 THEN (assume_tac 2));
    2.16 -by (fast_tac (!claset addSIs [equalityI]) 1);
    2.17 +by (Fast_tac 1);
    2.18  val eqpoll_sum_imp_Diff_eqpoll_lemma = result();
    2.19  
    2.20  goal thy "!!k. [| A eqpoll succ(k #+ m); B<=A; succ(k) eqpoll B;  \
    2.21 @@ -347,7 +347,7 @@
    2.22  
    2.23  goal thy "!!w. [| x Int y = 0; w <= x Un y |]  \
    2.24  \        ==> w Int (x - {u}) = w - cons(u, w Int y)";
    2.25 -by (fast_tac (!claset addSIs [equalityI] addEs [equals0D]) 1);
    2.26 +by (fast_tac (!claset addEs [equals0D]) 1);
    2.27  val w_Int_eq_w_Diff = result();
    2.28  
    2.29  goal thy "!!w. [| w:{v:s_u(u, t_n, succ(l), y). a <= v};  \
    2.30 @@ -440,7 +440,7 @@
    2.31  
    2.32  goal thy "{x:Pow(X). x lepoll 0} = {0}";
    2.33  by (fast_tac (!claset addSDs [lepoll_0_is_0]
    2.34 -                    addSIs [lepoll_refl, equalityI]) 1);
    2.35 +                      addSIs [lepoll_refl]) 1);
    2.36  val subsets_lepoll_0_eq_unit = result();
    2.37  
    2.38  goal thy "!!X. [| well_ord(X, R); ~Finite(X); n:nat |]  \
    2.39 @@ -453,8 +453,7 @@
    2.40  
    2.41  goal thy "!!n. n:nat ==> {z:Pow(y). z lepoll succ(n)} =  \
    2.42  \       {z:Pow(y). z lepoll n} Un {z:Pow(y). z eqpoll succ(n)}";
    2.43 -by (fast_tac (!claset addIs [le_refl, leI,
    2.44 -                le_imp_lepoll, equalityI]
    2.45 +by (fast_tac (!claset addIs [le_refl, leI, le_imp_lepoll]
    2.46                  addSDs [lepoll_succ_disj]
    2.47                  addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1);
    2.48  val subsets_lepoll_succ = result();
    2.49 @@ -476,7 +475,7 @@
    2.50  val tot_ord_unit = result();
    2.51  
    2.52  goalw thy [wf_on_def, wf_def] "wf[{a}](0)";
    2.53 -by (fast_tac (!claset addSIs [equalityI]) 1);
    2.54 +by (Fast_tac 1);
    2.55  val wf_on_unit = result();
    2.56  
    2.57  goalw thy [well_ord_def] "well_ord({a},0)";
     3.1 --- a/src/ZF/AC/AC16_lemmas.ML	Wed Jan 08 15:17:25 1997 +0100
     3.2 +++ b/src/ZF/AC/AC16_lemmas.ML	Thu Jan 09 10:20:03 1997 +0100
     3.3 @@ -8,7 +8,7 @@
     3.4  open AC16_lemmas;
     3.5  
     3.6  goal thy "!!a. a~:A ==> cons(a,A)-{a}=A";
     3.7 -by (fast_tac (!claset addSIs [equalityI]) 1);
     3.8 +by (Fast_tac 1);
     3.9  val cons_Diff_eq = result();
    3.10  
    3.11  goalw thy [lepoll_def] "1 lepoll X <-> (EX x. x:X)";
    3.12 @@ -94,7 +94,7 @@
    3.13  val prems = goal thy "(!!y. y:z ==> Ord(y)) ==> z <= succ(Union(z))";
    3.14  by (rtac subsetI 1);
    3.15  by (res_inst_tac [("Q","ALL y:z. y<=x")] (excluded_middle RS disjE) 1);
    3.16 -by (fast_tac (!claset addSIs [equalityI]) 2);
    3.17 +by (Fast_tac 2);
    3.18  by (etac swap 1);
    3.19  by (rtac ballI 1);
    3.20  by (rtac Ord_linear_le 1);
    3.21 @@ -114,16 +114,15 @@
    3.22  val succ_Union_not_mem = result();
    3.23  
    3.24  goal thy "Union(cons(succ(Union(z)),z)) = succ(Union(z))";
    3.25 -by (fast_tac (!claset addIs [equalityI]) 1);
    3.26 +by (Fast_tac 1);
    3.27  val Union_cons_eq_succ_Union = result();
    3.28  
    3.29  goal thy "!!i. [| Ord(i); Ord(j) |] ==> i Un j = i | i Un j = j";
    3.30 -by (fast_tac (!claset addSDs [le_imp_subset] addIs [equalityI]
    3.31 -                addEs [Ord_linear_le]) 1);
    3.32 +by (fast_tac (!claset addSDs [le_imp_subset] addEs [Ord_linear_le]) 1);
    3.33  val Un_Ord_disj = result();
    3.34  
    3.35  goal thy "!!X. x:X ==> Union(X) = x Un Union(X-{x})";
    3.36 -by (fast_tac (!claset addIs [equalityI]) 1);
    3.37 +by (Fast_tac 1);
    3.38  val Union_eq_Un = result();
    3.39  
    3.40  goal thy "!!n. n:nat ==>  \
    3.41 @@ -208,12 +207,12 @@
    3.42  
    3.43  goalw thy [surj_def] "!!f. [| f:surj(A,B); y<=B |]  \
    3.44  \       ==> f``(converse(f)``y) = y";
    3.45 -by (fast_tac (!claset addSIs [equalityI] addDs [apply_equality2]
    3.46 -        addEs [apply_iff RS iffD2]) 1);
    3.47 +by (fast_tac (!claset addDs [apply_equality2]
    3.48 +	              addEs [apply_iff RS iffD2]) 1);
    3.49  val image_vimage_eq = result();
    3.50  
    3.51  goal thy "!!f. [| f:inj(A,B); y<=A |] ==> converse(f)``(f``y) = y";
    3.52 -by (fast_tac (!claset addSIs [equalityI] addSEs [inj_is_fun RS apply_Pair]
    3.53 +by (fast_tac (!claset addSEs [inj_is_fun RS apply_Pair]
    3.54                  addDs [inj_equality]) 1);
    3.55  val vimage_image_eq = result();
    3.56  
     4.1 --- a/src/ZF/AC/AC17_AC1.ML	Wed Jan 08 15:17:25 1997 +0100
     4.2 +++ b/src/ZF/AC/AC17_AC1.ML	Thu Jan 09 10:20:03 1997 +0100
     4.3 @@ -56,8 +56,7 @@
     4.4  goal thy "!!x. ~ (EX f: Pow(x)-{0}->x. x - F(f) = 0)  \
     4.5  \       ==> (lam f: Pow(x)-{0}->x. x - F(f))  \
     4.6  \               : (Pow(x) -{0} -> x) -> Pow(x) - {0}";
     4.7 -by (fast_tac (!claset addSIs [lam_type] addIs [equalityI]
     4.8 -                addSDs [Diff_eq_0_iff RS iffD1]) 1);
     4.9 +by (fast_tac (!claset addSIs [lam_type] addSDs [Diff_eq_0_iff RS iffD1]) 1);
    4.10  val lemma2 = result();
    4.11  
    4.12  goal thy "!!f. [| f`Z : Z; Z:Pow(x)-{0} |] ==>  \
     5.1 --- a/src/ZF/AC/AC18_AC19.ML	Wed Jan 08 15:17:25 1997 +0100
     5.2 +++ b/src/ZF/AC/AC18_AC19.ML	Thu Jan 09 10:20:03 1997 +0100
     5.3 @@ -37,7 +37,7 @@
     5.4  
     5.5  val [prem] = goalw thy (AC18_def::AC_defs) "AC1 ==> AC18";
     5.6  by (resolve_tac [prem RS revcut_rl] 1);
     5.7 -by (fast_tac (!claset addSEs [lemma_AC18, UN_E, not_emptyE, apply_type]
     5.8 +by (fast_tac (!claset addSEs [lemma_AC18, not_emptyE, apply_type]
     5.9                  addSIs [equalityI, INT_I, UN_I]) 1);
    5.10  qed "AC1_AC18";
    5.11  
    5.12 @@ -70,7 +70,7 @@
    5.13  by (rtac subsetI 1);
    5.14  by (excluded_middle_tac "x=0" 1);
    5.15  by (Fast_tac 1);
    5.16 -by (fast_tac (!claset addEs [notE, subst_elem] addSIs [equalityI])  1);
    5.17 +by (fast_tac (!claset addEs [notE, subst_elem])  1);
    5.18  val lemma1_1 = result();
    5.19  
    5.20  goalw thy [u_def]
     6.1 --- a/src/ZF/AC/AC2_AC6.ML	Wed Jan 08 15:17:25 1997 +0100
     6.2 +++ b/src/ZF/AC/AC2_AC6.ML	Thu Jan 09 10:20:03 1997 +0100
     6.3 @@ -91,14 +91,11 @@
     6.4  val lemma1 = result();
     6.5  
     6.6  goal thy "!!f. domain(UN z:A. {z}*f(z)) = {a:A. f(a)~=0}";
     6.7 -by (fast_tac (!claset addIs [equalityI]
     6.8 -                addSEs [not_emptyE]
     6.9 -                addSIs [not_emptyI]
    6.10 -                addDs [range_type]) 1);
    6.11 +by (fast_tac (!claset addSIs [not_emptyI] addDs [range_type]) 1);
    6.12  val lemma2 = result();
    6.13  
    6.14  goal thy "!!f. x:A ==> (UN z:A. {z}*f(z))``{x} = f(x)";
    6.15 -by (fast_tac (!claset addIs [equalityI]) 1);
    6.16 +by (Fast_tac 1);
    6.17  val lemma3 = result();
    6.18  
    6.19  goalw thy AC_defs "!!Z. AC4 ==> AC3";
    6.20 @@ -116,7 +113,7 @@
    6.21  goal thy "!!A. b~:A ==> (PROD x:{a:A. id(A)`a~=b}. id(A)`x) = (PROD x:A. x)";
    6.22  by (asm_full_simp_tac (!simpset addsimps [id_def] addcongs [Pi_cong]) 1);
    6.23  by (res_inst_tac [("b","A")] subst_context 1);
    6.24 -by (fast_tac (!claset addSIs [equalityI]) 1);
    6.25 +by (Fast_tac 1);
    6.26  val lemma = result();
    6.27  
    6.28  goalw thy AC_defs "!!Z. AC3 ==> AC1";
     7.1 --- a/src/ZF/AC/AC_Equiv.ML	Wed Jan 08 15:17:25 1997 +0100
     7.2 +++ b/src/ZF/AC/AC_Equiv.ML	Thu Jan 09 10:20:03 1997 +0100
     7.3 @@ -150,9 +150,9 @@
     7.4  
     7.5  goalw thy [surj_def] "!!f. f : surj(A, B) ==> f``A = B";
     7.6  by (etac CollectE 1);
     7.7 -by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1 THEN (assume_tac 1));
     7.8 -by (fast_tac (!claset addSEs [RepFunE, apply_type]
     7.9 -                addSIs [RepFunI] addIs [equalityI]) 1);
    7.10 +by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1 
    7.11 +    THEN (assume_tac 1));
    7.12 +by (fast_tac (!claset addSEs [apply_type] addIs [equalityI]) 1);
    7.13  val surj_image_eq = result();
    7.14  
    7.15  
     8.1 --- a/src/ZF/AC/Cardinal_aux.ML	Wed Jan 08 15:17:25 1997 +0100
     8.2 +++ b/src/ZF/AC/Cardinal_aux.ML	Thu Jan 09 10:20:03 1997 +0100
     8.3 @@ -75,8 +75,7 @@
     8.4  goal upair.thy "if({y,z}-{z}=0, z, THE w. {y,z}-{z}={w}) = y";
     8.5  by (split_tac [expand_if] 1);
     8.6  by (asm_full_simp_tac (!simpset addsimps [double_Diff_sing, Diff_eq_0_iff]) 1);
     8.7 -by (fast_tac (!claset addSIs [the_equality, equalityI, equals0I]
     8.8 -                addEs [equalityE]) 1);
     8.9 +by (fast_tac (!claset addSIs [the_equality] addEs [equalityE]) 1);
    8.10  val paired_bij_lemma = result();
    8.11  
    8.12  goal thy "(lam y:{{y,z}. y:x}. if(y-{z}=0, z, THE w. y-{z}={w}))  \
    8.13 @@ -120,7 +119,7 @@
    8.14  by (fast_tac (!claset addSIs [Diff_sing_lepoll, the_first_in]) 1);
    8.15  by (res_inst_tac [("b","y-{THE b. first(b, y, r)}")] subst 1);
    8.16  by (rtac empty_lepollI 2);
    8.17 -by (fast_tac (!claset addSIs [equalityI]) 1);
    8.18 +by (Fast_tac 1);
    8.19  val Diff_first_lepoll = result();
    8.20  
    8.21  goal thy "(UN x:X. P(x)) <= (UN x:X. P(x)-Q(x)) Un (UN x:X. Q(x))";
     9.1 --- a/src/ZF/AC/DC.ML	Wed Jan 08 15:17:25 1997 +0100
     9.2 +++ b/src/ZF/AC/DC.ML	Thu Jan 09 10:20:03 1997 +0100
     9.3 @@ -316,7 +316,7 @@
     9.4  goal thy "!!f. [| (UN x:f``n. P(x)) = y; P(f`n) = succ(y);  \
     9.5  \       f:nat -> X; n:nat |] ==> (UN x:f``succ(n). P(x)) = succ(y)";
     9.6  by (asm_full_simp_tac (!simpset addsimps [UN_image_succ_eq]) 1);
     9.7 -by (fast_tac (!claset addSIs [equalityI]) 1);
     9.8 +by (Fast_tac 1);
     9.9  val UN_image_succ_eq_succ = result();
    9.10  
    9.11  goal thy "!!f. [| f:succ(n) -> D;  n:nat;  \
    10.1 --- a/src/ZF/AC/DC_lemmas.ML	Wed Jan 08 15:17:25 1997 +0100
    10.2 +++ b/src/ZF/AC/DC_lemmas.ML	Thu Jan 09 10:20:03 1997 +0100
    10.3 @@ -55,7 +55,7 @@
    10.4  val cons_fun_type2 = result();
    10.5  
    10.6  goal thy "!!n. n: nat ==> cons(<n,x>, g)``n = g``n";
    10.7 -by (fast_tac (!claset addSIs [equalityI] addSEs [mem_irrefl]) 1);
    10.8 +by (fast_tac (!claset addSEs [mem_irrefl]) 1);
    10.9  val cons_image_n = result();
   10.10  
   10.11  goal thy "!!n. g:n->X ==> cons(<n,x>, g)`n = x";
   10.12 @@ -63,7 +63,7 @@
   10.13  val cons_val_n = result();
   10.14  
   10.15  goal thy "!!k. k : n ==> cons(<n,x>, g)``k = g``k";
   10.16 -by (fast_tac (!claset addSIs [equalityI] addEs [mem_asym]) 1);
   10.17 +by (fast_tac (!claset addEs [mem_asym]) 1);
   10.18  val cons_image_k = result();
   10.19  
   10.20  goal thy "!!k. [| k:n; g:n->X |] ==> cons(<n,x>, g)`k = g`k";
    11.1 --- a/src/ZF/AC/HH.ML	Wed Jan 08 15:17:25 1997 +0100
    11.2 +++ b/src/ZF/AC/HH.ML	Thu Jan 09 10:20:03 1997 +0100
    11.3 @@ -29,7 +29,7 @@
    11.4  val HH_values = result();
    11.5  
    11.6  goal thy "!!A. B<=A ==> X-(UN a:A. P(a)) = X-(UN a:A-B. P(a))-(UN b:B. P(b))";
    11.7 -by (fast_tac (!claset addSIs [equalityI]) 1);
    11.8 +by (Fast_tac 1);
    11.9  val subset_imp_Diff_eq = result();
   11.10  
   11.11  goal thy "!!c. [| c:a-b; b<a |] ==> c=b | b<c & c<a";
   11.12 @@ -41,8 +41,7 @@
   11.13  
   11.14  val prems = goal thy "(!!y. y:A ==> P(y) = {x}) ==> x - (UN y:A. P(y)) = x";
   11.15  by (asm_full_simp_tac (!simpset addsimps prems) 1);
   11.16 -by (fast_tac (!claset addSIs [equalityI] addSDs [prem]
   11.17 -                addSEs [RepFunE, mem_irrefl]) 1);
   11.18 +by (fast_tac (!claset addSDs [prem] addSEs [mem_irrefl]) 1);
   11.19  val Diff_UN_eq_self = result();
   11.20  
   11.21  goal thy "!!a. x - (UN b:a. HH(f,x,b)) = x - (UN b:a1. HH(f,x,b))  \
    12.1 --- a/src/ZF/AC/WO1_AC.ML	Wed Jan 08 15:17:25 1997 +0100
    12.2 +++ b/src/ZF/AC/WO1_AC.ML	Thu Jan 09 10:20:03 1997 +0100
    12.3 @@ -101,8 +101,7 @@
    12.4  
    12.5  goalw thy [bij_def, surj_def]
    12.6          "!!f. f : bij(D+D, B) ==> Union({{f`Inl(i), f`Inr(i)}. i:D})=B";
    12.7 -by (fast_tac (!claset addSEs [inj_is_fun RS apply_type, CollectE, sumE]
    12.8 -        addSIs [InlI, InrI, equalityI]) 1);
    12.9 +by (fast_tac (!claset addSEs [inj_is_fun RS apply_type]) 1);
   12.10  val lemma2_5 = result();
   12.11  
   12.12  goal thy "!!A. [| WO1; ~Finite(B); 1 le n  |]  \
    13.1 --- a/src/ZF/AC/WO1_WO6.ML	Wed Jan 08 15:17:25 1997 +0100
    13.2 +++ b/src/ZF/AC/WO1_WO6.ML	Thu Jan 09 10:20:03 1997 +0100
    13.3 @@ -37,12 +37,12 @@
    13.4  val lam_sets = result();
    13.5  
    13.6  goalw thy [surj_def] "!!f. f:surj(A,B) ==> (UN a:A. {f`a}) = B";
    13.7 -by (fast_tac (!claset addSIs [equalityI] addSEs [apply_type]) 1);
    13.8 +by (fast_tac (!claset addSEs [apply_type]) 1);
    13.9  val surj_imp_eq_ = result();
   13.10  
   13.11  goal thy "!!f. [| f:surj(A,B); Ord(A) |] ==> (UN a<A. {f`a}) = B";
   13.12  by (fast_tac (!claset addSDs [surj_imp_eq_]
   13.13 -                addSIs [equalityI, ltI] addSEs [ltE]) 1);
   13.14 +                addSIs [ltI] addSEs [ltE]) 1);
   13.15  val surj_imp_eq = result();
   13.16  
   13.17  goalw thy WO_defs "!!Z. WO1 ==> WO4(1)";
    14.1 --- a/src/ZF/AC/WO2_AC16.ML	Wed Jan 08 15:17:25 1997 +0100
    14.2 +++ b/src/ZF/AC/WO2_AC16.ML	Thu Jan 09 10:20:03 1997 +0100
    14.3 @@ -191,7 +191,7 @@
    14.4  val Un_lepoll_succ = result();
    14.5  
    14.6  goal thy "!!a. Ord(a) ==> F(a) - (UN b<succ(a). F(b)) = 0";
    14.7 -by (fast_tac (!claset addSIs [OUN_I, le_refl] addIs [equalityI]) 1);
    14.8 +by (fast_tac (!claset addSIs [OUN_I, le_refl]) 1);
    14.9  val Diff_UN_succ_empty = result();
   14.10  
   14.11  goal thy "!!a. Ord(a) ==> F(a) Un X - (UN b<succ(a). F(b)) <= X";
   14.12 @@ -366,7 +366,7 @@
   14.13  
   14.14  goal thy "!!A. m:nat ==> ALL A B. A <= B & m lepoll A & B lepoll m --> A=B";
   14.15  by (etac nat_induct 1);
   14.16 -by (fast_tac (!claset addSDs [lepoll_0_is_0] addSIs [equalityI]) 1);
   14.17 +by (fast_tac (!claset addSDs [lepoll_0_is_0]) 1);
   14.18  by (REPEAT (resolve_tac [allI, impI] 1));
   14.19  by (REPEAT (etac conjE 1));
   14.20  by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1
    15.1 --- a/src/ZF/Epsilon.ML	Wed Jan 08 15:17:25 1997 +0100
    15.2 +++ b/src/ZF/Epsilon.ML	Thu Jan 09 10:20:03 1997 +0100
    15.3 @@ -228,7 +228,7 @@
    15.4  
    15.5  goal Epsilon.thy "rank(0) = 0";
    15.6  by (rtac (rank RS trans) 1);
    15.7 -by (fast_tac (!claset addSIs [equalityI]) 1);
    15.8 +by (Fast_tac 1);
    15.9  qed "rank_0";
   15.10  
   15.11  goal Epsilon.thy "rank(succ(x)) = succ(rank(x))";
    16.1 --- a/src/ZF/EquivClass.ML	Wed Jan 08 15:17:25 1997 +0100
    16.2 +++ b/src/ZF/EquivClass.ML	Thu Jan 09 10:20:03 1997 +0100
    16.3 @@ -26,8 +26,7 @@
    16.4  
    16.5  goalw EquivClass.thy [equiv_def]
    16.6      "!!A r. equiv(A,r) ==> converse(r) O r = r";
    16.7 -by (fast_tac (subset_cs addSIs [equalityI, sym_trans_comp_subset, 
    16.8 -                                refl_comp_subset]) 1);
    16.9 +by (fast_tac (subset_cs addSIs [sym_trans_comp_subset, refl_comp_subset]) 1);
   16.10  qed "equiv_comp_eq";
   16.11  
   16.12  (*second half*)
    17.1 --- a/src/ZF/IMP/Equiv.ML	Wed Jan 08 15:17:25 1997 +0100
    17.2 +++ b/src/ZF/IMP/Equiv.ML	Thu Jan 09 10:20:03 1997 +0100
    17.3 @@ -120,7 +120,7 @@
    17.4  
    17.5  goal Equiv.thy
    17.6      "ALL c:com. C(c) = {io:(loc->nat)*(loc->nat). <c,fst(io)> -c-> snd(io)}";
    17.7 -by (fast_tac (!claset addIs [equalityI, C_subset RS subsetD]
    17.8 +by (fast_tac (!claset addIs [C_subset RS subsetD]
    17.9  	              addEs [com2 RS bspec]
   17.10  		      addDs [com1]
   17.11  		      addss (!simpset)) 1);
    18.1 --- a/src/ZF/List.ML	Wed Jan 08 15:17:25 1997 +0100
    18.2 +++ b/src/ZF/List.ML	Thu Jan 09 10:20:03 1997 +0100
    18.3 @@ -28,8 +28,7 @@
    18.4  
    18.5  goal List.thy "list(A) = {0} + (A * list(A))";
    18.6  let open list;  val rew = rewrite_rule con_defs in  
    18.7 -by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
    18.8 -                     addEs [rew elim]) 1)
    18.9 +by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
   18.10  end;
   18.11  qed "list_unfold";
   18.12  
    19.1 --- a/src/ZF/ex/Brouwer.ML	Wed Jan 08 15:17:25 1997 +0100
    19.2 +++ b/src/ZF/ex/Brouwer.ML	Thu Jan 09 10:20:03 1997 +0100
    19.3 @@ -14,8 +14,7 @@
    19.4  
    19.5  goal Brouwer.thy "brouwer = {0} + brouwer + (nat -> brouwer)";
    19.6  let open brouwer;  val rew = rewrite_rule con_defs in  
    19.7 -by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
    19.8 -                     addEs [rew elim]) 1)
    19.9 +by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
   19.10  end;
   19.11  qed "brouwer_unfold";
   19.12  
   19.13 @@ -38,8 +37,7 @@
   19.14  
   19.15  goal Brouwer.thy "Well(A,B) = (SUM x:A. B(x) -> Well(A,B))";
   19.16  let open Well;  val rew = rewrite_rule con_defs in  
   19.17 -by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
   19.18 -                     addEs [rew elim]) 1)
   19.19 +by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
   19.20  end;
   19.21  qed "Well_unfold";
   19.22  
    20.1 --- a/src/ZF/ex/Comb.ML	Wed Jan 08 15:17:25 1997 +0100
    20.2 +++ b/src/ZF/ex/Comb.ML	Thu Jan 09 10:20:03 1997 +0100
    20.3 @@ -29,7 +29,7 @@
    20.4  val contract_combD2 = contract.dom_subset RS subsetD RS SigmaD2;
    20.5  
    20.6  goal Comb.thy "field(contract) = comb";
    20.7 -by (fast_tac (!claset addIs [equalityI,contract.K] addSEs [contract_combE2]) 1);
    20.8 +by (fast_tac (!claset addIs [contract.K] addSEs [contract_combE2]) 1);
    20.9  qed "field_contract_eq";
   20.10  
   20.11  bind_thm ("reduction_refl",
   20.12 @@ -121,8 +121,8 @@
   20.13  val parcontract_combD2 = parcontract.dom_subset RS subsetD RS SigmaD2;
   20.14  
   20.15  goal Comb.thy "field(parcontract) = comb";
   20.16 -by (fast_tac (!claset addIs [equalityI, parcontract.K] 
   20.17 -                    addSEs [parcontract_combE2]) 1);
   20.18 +by (fast_tac (!claset addIs [parcontract.K] 
   20.19 +                      addSEs [parcontract_combE2]) 1);
   20.20  qed "field_parcontract_eq";
   20.21  
   20.22  (*Derive a case for each combinator constructor*)
    21.1 --- a/src/ZF/ex/Data.ML	Wed Jan 08 15:17:25 1997 +0100
    21.2 +++ b/src/ZF/ex/Data.ML	Thu Jan 09 10:20:03 1997 +0100
    21.3 @@ -11,8 +11,7 @@
    21.4  
    21.5  goal Data.thy "data(A,B) = ({0} + A) + (A*B + A*B*data(A,B))";
    21.6  let open data;  val rew = rewrite_rule con_defs in  
    21.7 -by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
    21.8 -                     addEs [rew elim]) 1)
    21.9 +by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
   21.10  end;
   21.11  qed "data_unfold";
   21.12  
    22.1 --- a/src/ZF/ex/LList.ML	Wed Jan 08 15:17:25 1997 +0100
    22.2 +++ b/src/ZF/ex/LList.ML	Thu Jan 09 10:20:03 1997 +0100
    22.3 @@ -23,8 +23,7 @@
    22.4  
    22.5  goal LList.thy "llist(A) = {0} <+> (A <*> llist(A))";
    22.6  let open llist;  val rew = rewrite_rule con_defs in  
    22.7 -by (fast_tac (!claset addSIs (subsetI :: equalityI :: map rew intrs)
    22.8 -                      addEs [rew elim]) 1)
    22.9 +by (fast_tac (!claset addSIs (subsetI ::map rew intrs) addEs [rew elim]) 1)
   22.10  end;
   22.11  qed "llist_unfold";
   22.12  
    23.1 --- a/src/ZF/ex/Ntree.ML	Wed Jan 08 15:17:25 1997 +0100
    23.2 +++ b/src/ZF/ex/Ntree.ML	Thu Jan 09 10:20:03 1997 +0100
    23.3 @@ -15,8 +15,7 @@
    23.4  
    23.5  goal Ntree.thy "ntree(A) = A * (UN n: nat. n -> ntree(A))";
    23.6  let open ntree;  val rew = rewrite_rule con_defs in  
    23.7 -by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
    23.8 -                     addEs [rew elim]) 1)
    23.9 +by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
   23.10  end;
   23.11  qed "ntree_unfold";
   23.12  
   23.13 @@ -70,8 +69,7 @@
   23.14  
   23.15  goal Ntree.thy "maptree(A) = A * (maptree(A) -||> maptree(A))";
   23.16  let open maptree;  val rew = rewrite_rule con_defs in  
   23.17 -by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
   23.18 -                     addEs [rew elim]) 1)
   23.19 +by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
   23.20  end;
   23.21  qed "maptree_unfold";
   23.22  
   23.23 @@ -95,8 +93,7 @@
   23.24  
   23.25  goal Ntree.thy "maptree2(A,B) = A * (B -||> maptree2(A,B))";
   23.26  let open maptree2;  val rew = rewrite_rule con_defs in  
   23.27 -by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
   23.28 -                     addEs [rew elim]) 1)
   23.29 +by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
   23.30  end;
   23.31  qed "maptree2_unfold";
   23.32  
    24.1 --- a/src/ZF/ex/TF.ML	Wed Jan 08 15:17:25 1997 +0100
    24.2 +++ b/src/ZF/ex/TF.ML	Thu Jan 09 10:20:03 1997 +0100
    24.3 @@ -38,8 +38,7 @@
    24.4      "tree_forest(A) = (A*forest(A)) + ({0} + tree(A)*forest(A))";
    24.5  let open tree_forest;  
    24.6      val rew = rewrite_rule (con_defs @ tl defs) in  
    24.7 -by (fast_tac (!claset addSIs (equalityI :: (map rew intrs RL [PartD1]))
    24.8 -                     addEs [rew elim]) 1)
    24.9 +by (fast_tac (!claset addSIs (map rew intrs RL [PartD1]) addEs [rew elim]) 1)
   24.10  end;
   24.11  qed "tree_forest_unfold";
   24.12  
    25.1 --- a/src/ZF/ex/Term.ML	Wed Jan 08 15:17:25 1997 +0100
    25.2 +++ b/src/ZF/ex/Term.ML	Thu Jan 09 10:20:03 1997 +0100
    25.3 @@ -11,8 +11,7 @@
    25.4  
    25.5  goal Term.thy "term(A) = A * list(term(A))";
    25.6  let open term;  val rew = rewrite_rule con_defs in  
    25.7 -by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
    25.8 -                     addEs [rew elim]) 1)
    25.9 +by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1)
   25.10  end;
   25.11  qed "term_unfold";
   25.12  
    26.1 --- a/src/ZF/ex/misc.ML	Wed Jan 08 15:17:25 1997 +0100
    26.2 +++ b/src/ZF/ex/misc.ML	Thu Jan 09 10:20:03 1997 +0100
    26.3 @@ -145,9 +145,7 @@
    26.4  \    : bij(Pow(A+B), Pow(A)*Pow(B))";
    26.5  by (res_inst_tac [("d", "%<X,Y>.{Inl(x).x:X} Un {Inr(y).y:Y}")] 
    26.6      lam_bijective 1);
    26.7 -by (TRYALL (etac SigmaE));
    26.8 -by (ALLGOALS Asm_simp_tac);
    26.9 -by (ALLGOALS (fast_tac (!claset addSIs [equalityI])));
   26.10 +by (Auto_tac());
   26.11  val Pow_bij = result();
   26.12  
   26.13  writeln"Reached end of file.";
    27.1 --- a/src/ZF/simpdata.ML	Wed Jan 08 15:17:25 1997 +0100
    27.2 +++ b/src/ZF/simpdata.ML	Thu Jan 09 10:20:03 1997 +0100
    27.3 @@ -11,8 +11,7 @@
    27.4  (*For proving rewrite rules*)
    27.5  fun prove_fun s = 
    27.6      (writeln s;  prove_goal thy s
    27.7 -       (fn prems => [ (cut_facts_tac prems 1), 
    27.8 -                      (fast_tac (!claset addSIs [equalityI]) 1) ]));
    27.9 +       (fn prems => [ (cut_facts_tac prems 1), (Fast_tac 1) ]));
   27.10  
   27.11  (*Are all these really suitable?*)
   27.12  val ball_simps = map prove_fun