Ran expandshort
authorpaulson
Wed Mar 06 13:57:07 1996 +0100 (1996-03-06 ago)
changeset 15534eb4a9c7d736
parent 1552 6f71b5d46700
child 1554 4ee99a973be4
Ran expandshort
src/HOL/Finite.ML
src/HOL/equalities.ML
     1.1 --- a/src/HOL/Finite.ML	Wed Mar 06 12:52:11 1996 +0100
     1.2 +++ b/src/HOL/Finite.ML	Wed Mar 06 13:57:07 1996 +0100
     1.3 @@ -55,15 +55,15 @@
     1.4  qed "Fin_subset";
     1.5  
     1.6  goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";
     1.7 -by(fast_tac (set_cs addIs [Fin_UnI] addDs
     1.8 +by (fast_tac (set_cs addIs [Fin_UnI] addDs
     1.9                  [Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
    1.10  qed "subset_Fin";
    1.11  Addsimps[subset_Fin];
    1.12  
    1.13  goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)";
    1.14 -by(stac insert_is_Un 1);
    1.15 -by(Simp_tac 1);
    1.16 -by(fast_tac (set_cs addSIs Fin.intrs addDs [FinD]) 1);
    1.17 +by (stac insert_is_Un 1);
    1.18 +by (Simp_tac 1);
    1.19 +by (fast_tac (set_cs addSIs Fin.intrs addDs [FinD]) 1);
    1.20  qed "insert_Fin";
    1.21  Addsimps[insert_Fin];
    1.22  
    1.23 @@ -110,47 +110,47 @@
    1.24  
    1.25  
    1.26  goalw Finite.thy [finite_def] "finite {}";
    1.27 -by(Simp_tac 1);
    1.28 +by (Simp_tac 1);
    1.29  qed "finite_emptyI";
    1.30  Addsimps [finite_emptyI];
    1.31  
    1.32  goalw Finite.thy [finite_def] "!!A. finite A ==> finite(insert a A)";
    1.33 -by(Asm_simp_tac 1);
    1.34 +by (Asm_simp_tac 1);
    1.35  qed "finite_insertI";
    1.36  
    1.37  (*The union of two finite sets is finite*)
    1.38  goalw Finite.thy [finite_def]
    1.39      "!!F. [| finite F;  finite G |] ==> finite(F Un G)";
    1.40 -by(Asm_simp_tac 1);
    1.41 +by (Asm_simp_tac 1);
    1.42  qed "finite_UnI";
    1.43  
    1.44  goalw Finite.thy [finite_def] "!!A. [| A<=B;  finite B |] ==> finite A";
    1.45 -be Fin_subset 1;
    1.46 -ba 1;
    1.47 +by (etac Fin_subset 1);
    1.48 +by (assume_tac 1);
    1.49  qed "finite_subset";
    1.50  
    1.51  goalw Finite.thy [finite_def] "finite(F Un G) = (finite F & finite G)";
    1.52 -by(Simp_tac 1);
    1.53 +by (Simp_tac 1);
    1.54  qed "subset_finite";
    1.55  Addsimps[subset_finite];
    1.56  
    1.57  goalw Finite.thy [finite_def] "finite(insert a A) = finite(A)";
    1.58 -by(Simp_tac 1);
    1.59 +by (Simp_tac 1);
    1.60  qed "insert_finite";
    1.61  Addsimps[insert_finite];
    1.62  
    1.63  goal Finite.thy "!!A. finite(A) ==> finite(A-B)";
    1.64 -be finite_induct 1;
    1.65 -by(Simp_tac 1);
    1.66 -by(asm_simp_tac (!simpset addsimps [insert_Diff_if]
    1.67 +by (etac finite_induct 1);
    1.68 +by (Simp_tac 1);
    1.69 +by (asm_simp_tac (!simpset addsimps [insert_Diff_if]
    1.70                            setloop split_tac[expand_if]) 1);
    1.71  qed "finite_Diff";
    1.72  Addsimps [finite_Diff];
    1.73  
    1.74  (*The image of a finite set is finite*)
    1.75  goal Finite.thy "!!F. finite F ==> finite(h``F)";
    1.76 -be finite_induct 1;
    1.77 -by(ALLGOALS Asm_simp_tac);
    1.78 +by (etac finite_induct 1);
    1.79 +by (ALLGOALS Asm_simp_tac);
    1.80  qed "finite_imageI";
    1.81  
    1.82  val major::prems = goalw Finite.thy [finite_def]
    1.83 @@ -166,152 +166,152 @@
    1.84  section "Finite cardinality -- 'card'";
    1.85  
    1.86  goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
    1.87 -by(fast_tac eq_cs 1);
    1.88 +by (fast_tac eq_cs 1);
    1.89  val Collect_conv_insert = result();
    1.90  
    1.91  goalw Finite.thy [card_def] "card {} = 0";
    1.92 -br Least_equality 1;
    1.93 -by(ALLGOALS Asm_full_simp_tac);
    1.94 +by (rtac Least_equality 1);
    1.95 +by (ALLGOALS Asm_full_simp_tac);
    1.96  qed "card_empty";
    1.97  Addsimps [card_empty];
    1.98  
    1.99  val [major] = goal Finite.thy
   1.100    "finite A ==> ? (n::nat) f. A = {f i |i. i<n}";
   1.101 -br (major RS finite_induct) 1;
   1.102 - by(res_inst_tac [("x","0")] exI 1);
   1.103 - by(Simp_tac 1);
   1.104 -be exE 1;
   1.105 -be exE 1;
   1.106 -by(hyp_subst_tac 1);
   1.107 -by(res_inst_tac [("x","Suc n")] exI 1);
   1.108 -by(res_inst_tac [("x","%i. if i<n then f i else x")] exI 1);
   1.109 -by(asm_simp_tac (!simpset addsimps [Collect_conv_insert]
   1.110 +by (rtac (major RS finite_induct) 1);
   1.111 + by (res_inst_tac [("x","0")] exI 1);
   1.112 + by (Simp_tac 1);
   1.113 +by (etac exE 1);
   1.114 +by (etac exE 1);
   1.115 +by (hyp_subst_tac 1);
   1.116 +by (res_inst_tac [("x","Suc n")] exI 1);
   1.117 +by (res_inst_tac [("x","%i. if i<n then f i else x")] exI 1);
   1.118 +by (asm_simp_tac (!simpset addsimps [Collect_conv_insert]
   1.119                            addcongs [rev_conj_cong]) 1);
   1.120  qed "finite_has_card";
   1.121  
   1.122  goal Finite.thy
   1.123    "!!A.[| x ~: A; insert x A = {f i|i.i<n} |] ==> \
   1.124  \  ? m::nat. m<n & (? g. A = {g i|i.i<m})";
   1.125 -by(res_inst_tac [("n","n")] natE 1);
   1.126 - by(hyp_subst_tac 1);
   1.127 - by(Asm_full_simp_tac 1);
   1.128 -by(rename_tac "m" 1);
   1.129 -by(hyp_subst_tac 1);
   1.130 -by(case_tac "? a. a:A" 1);
   1.131 - by(res_inst_tac [("x","0")] exI 2);
   1.132 - by(Simp_tac 2);
   1.133 - by(fast_tac eq_cs 2);
   1.134 -be exE 1;
   1.135 -by(Simp_tac 1);
   1.136 -br exI 1;
   1.137 -br conjI 1;
   1.138 +by (res_inst_tac [("n","n")] natE 1);
   1.139 + by (hyp_subst_tac 1);
   1.140 + by (Asm_full_simp_tac 1);
   1.141 +by (rename_tac "m" 1);
   1.142 +by (hyp_subst_tac 1);
   1.143 +by (case_tac "? a. a:A" 1);
   1.144 + by (res_inst_tac [("x","0")] exI 2);
   1.145 + by (Simp_tac 2);
   1.146 + by (fast_tac eq_cs 2);
   1.147 +by (etac exE 1);
   1.148 +by (Simp_tac 1);
   1.149 +by (rtac exI 1);
   1.150 +by (rtac conjI 1);
   1.151   br disjI2 1;
   1.152   br refl 1;
   1.153 -be equalityE 1;
   1.154 -by(asm_full_simp_tac
   1.155 +by (etac equalityE 1);
   1.156 +by (asm_full_simp_tac
   1.157       (!simpset addsimps [subset_insert,Collect_conv_insert]) 1);
   1.158 -by(SELECT_GOAL(safe_tac eq_cs)1);
   1.159 -  by(Asm_full_simp_tac 1);
   1.160 -  by(res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
   1.161 -  by(SELECT_GOAL(safe_tac eq_cs)1);
   1.162 -   by(subgoal_tac "x ~= f m" 1);
   1.163 -    by(fast_tac set_cs 2);
   1.164 -   by(subgoal_tac "? k. f k = x & k<m" 1);
   1.165 -    by(best_tac set_cs 2);
   1.166 -   by(SELECT_GOAL(safe_tac HOL_cs)1);
   1.167 -   by(res_inst_tac [("x","k")] exI 1);
   1.168 -   by(Asm_simp_tac 1);
   1.169 -  by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   1.170 -  by(best_tac set_cs 1);
   1.171 +by (SELECT_GOAL(safe_tac eq_cs)1);
   1.172 +  by (Asm_full_simp_tac 1);
   1.173 +  by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
   1.174 +  by (SELECT_GOAL(safe_tac eq_cs)1);
   1.175 +   by (subgoal_tac "x ~= f m" 1);
   1.176 +    by (fast_tac set_cs 2);
   1.177 +   by (subgoal_tac "? k. f k = x & k<m" 1);
   1.178 +    by (best_tac set_cs 2);
   1.179 +   by (SELECT_GOAL(safe_tac HOL_cs)1);
   1.180 +   by (res_inst_tac [("x","k")] exI 1);
   1.181 +   by (Asm_simp_tac 1);
   1.182 +  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   1.183 +  by (best_tac set_cs 1);
   1.184   bd sym 1;
   1.185 - by(rotate_tac ~1 1);
   1.186 - by(Asm_full_simp_tac 1);
   1.187 - by(res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
   1.188 - by(SELECT_GOAL(safe_tac eq_cs)1);
   1.189 -  by(subgoal_tac "x ~= f m" 1);
   1.190 -   by(fast_tac set_cs 2);
   1.191 -  by(subgoal_tac "? k. f k = x & k<m" 1);
   1.192 -   by(best_tac set_cs 2);
   1.193 -  by(SELECT_GOAL(safe_tac HOL_cs)1);
   1.194 -  by(res_inst_tac [("x","k")] exI 1);
   1.195 -  by(Asm_simp_tac 1);
   1.196 - by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   1.197 - by(best_tac set_cs 1);
   1.198 -by(res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
   1.199 -by(SELECT_GOAL(safe_tac eq_cs)1);
   1.200 - by(subgoal_tac "x ~= f i" 1);
   1.201 -  by(fast_tac set_cs 2);
   1.202 - by(case_tac "x = f m" 1);
   1.203 -  by(res_inst_tac [("x","i")] exI 1);
   1.204 -  by(Asm_simp_tac 1);
   1.205 - by(subgoal_tac "? k. f k = x & k<m" 1);
   1.206 -  by(best_tac set_cs 2);
   1.207 - by(SELECT_GOAL(safe_tac HOL_cs)1);
   1.208 - by(res_inst_tac [("x","k")] exI 1);
   1.209 - by(Asm_simp_tac 1);
   1.210 -by(simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   1.211 -by(best_tac set_cs 1);
   1.212 + by (rotate_tac ~1 1);
   1.213 + by (Asm_full_simp_tac 1);
   1.214 + by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
   1.215 + by (SELECT_GOAL(safe_tac eq_cs)1);
   1.216 +  by (subgoal_tac "x ~= f m" 1);
   1.217 +   by (fast_tac set_cs 2);
   1.218 +  by (subgoal_tac "? k. f k = x & k<m" 1);
   1.219 +   by (best_tac set_cs 2);
   1.220 +  by (SELECT_GOAL(safe_tac HOL_cs)1);
   1.221 +  by (res_inst_tac [("x","k")] exI 1);
   1.222 +  by (Asm_simp_tac 1);
   1.223 + by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   1.224 + by (best_tac set_cs 1);
   1.225 +by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
   1.226 +by (SELECT_GOAL(safe_tac eq_cs)1);
   1.227 + by (subgoal_tac "x ~= f i" 1);
   1.228 +  by (fast_tac set_cs 2);
   1.229 + by (case_tac "x = f m" 1);
   1.230 +  by (res_inst_tac [("x","i")] exI 1);
   1.231 +  by (Asm_simp_tac 1);
   1.232 + by (subgoal_tac "? k. f k = x & k<m" 1);
   1.233 +  by (best_tac set_cs 2);
   1.234 + by (SELECT_GOAL(safe_tac HOL_cs)1);
   1.235 + by (res_inst_tac [("x","k")] exI 1);
   1.236 + by (Asm_simp_tac 1);
   1.237 +by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   1.238 +by (best_tac set_cs 1);
   1.239  val lemma = result();
   1.240  
   1.241  goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
   1.242  \ (LEAST n. ? f. insert x A = {f i|i.i<n}) = Suc(LEAST n. ? f. A={f i|i.i<n})";
   1.243 -br Least_equality 1;
   1.244 +by (rtac Least_equality 1);
   1.245   bd finite_has_card 1;
   1.246   be exE 1;
   1.247 - by(dres_inst_tac [("P","%n.? f. A={f i|i.i<n}")] LeastI 1);
   1.248 + by (dres_inst_tac [("P","%n.? f. A={f i|i.i<n}")] LeastI 1);
   1.249   be exE 1;
   1.250 - by(res_inst_tac
   1.251 + by (res_inst_tac
   1.252     [("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
   1.253 - by(simp_tac
   1.254 + by (simp_tac
   1.255      (!simpset addsimps [Collect_conv_insert] addcongs [rev_conj_cong]) 1);
   1.256   be subst 1;
   1.257   br refl 1;
   1.258 -br notI 1;
   1.259 -be exE 1;
   1.260 -bd lemma 1;
   1.261 +by (rtac notI 1);
   1.262 +by (etac exE 1);
   1.263 +by (dtac lemma 1);
   1.264   ba 1;
   1.265 -be exE 1;
   1.266 -be conjE 1;
   1.267 -by(dres_inst_tac [("P","%x. ? g. A = {g i |i. i < x}")] Least_le 1);
   1.268 -by(dtac le_less_trans 1 THEN atac 1);
   1.269 -by(Asm_full_simp_tac 1);
   1.270 -be disjE 1;
   1.271 -by(etac less_asym 1 THEN atac 1);
   1.272 -by(hyp_subst_tac 1);
   1.273 -by(Asm_full_simp_tac 1);
   1.274 +by (etac exE 1);
   1.275 +by (etac conjE 1);
   1.276 +by (dres_inst_tac [("P","%x. ? g. A = {g i |i. i < x}")] Least_le 1);
   1.277 +by (dtac le_less_trans 1 THEN atac 1);
   1.278 +by (Asm_full_simp_tac 1);
   1.279 +by (etac disjE 1);
   1.280 +by (etac less_asym 1 THEN atac 1);
   1.281 +by (hyp_subst_tac 1);
   1.282 +by (Asm_full_simp_tac 1);
   1.283  val lemma = result();
   1.284  
   1.285  goalw Finite.thy [card_def]
   1.286    "!!A. [| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)";
   1.287 -be lemma 1;
   1.288 -ba 1;
   1.289 +by (etac lemma 1);
   1.290 +by (assume_tac 1);
   1.291  qed "card_insert_disjoint";
   1.292  
   1.293  val [major] = goal Finite.thy
   1.294    "finite A ==> card(insert x A) = Suc(card(A-{x}))";
   1.295 -by(case_tac "x:A" 1);
   1.296 -by(asm_simp_tac (!simpset addsimps [insert_absorb]) 1);
   1.297 -bd mk_disjoint_insert 1;
   1.298 -be exE 1;
   1.299 -by(Asm_simp_tac 1);
   1.300 -br card_insert_disjoint 1;
   1.301 -br (major RSN (2,finite_subset)) 1;
   1.302 -by(fast_tac set_cs 1);
   1.303 -by(fast_tac HOL_cs 1);
   1.304 -by(asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1);
   1.305 +by (case_tac "x:A" 1);
   1.306 +by (asm_simp_tac (!simpset addsimps [insert_absorb]) 1);
   1.307 +by (dtac mk_disjoint_insert 1);
   1.308 +by (etac exE 1);
   1.309 +by (Asm_simp_tac 1);
   1.310 +by (rtac card_insert_disjoint 1);
   1.311 +by (rtac (major RSN (2,finite_subset)) 1);
   1.312 +by (fast_tac set_cs 1);
   1.313 +by (fast_tac HOL_cs 1);
   1.314 +by (asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1);
   1.315  qed "card_insert";
   1.316  Addsimps [card_insert];
   1.317  
   1.318  
   1.319  goal Finite.thy  "!!A. finite A ==> !B. B <= A --> card(B) <= card(A)";
   1.320 -be finite_induct 1;
   1.321 -by(Simp_tac 1);
   1.322 -by(strip_tac 1);
   1.323 -by(case_tac "x:B" 1);
   1.324 - bd mk_disjoint_insert 1;
   1.325 - by(SELECT_GOAL(safe_tac HOL_cs)1);
   1.326 - by(rotate_tac ~1 1);
   1.327 - by(asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
   1.328 -by(rotate_tac ~1 1);
   1.329 -by(asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
   1.330 +by (etac finite_induct 1);
   1.331 +by (Simp_tac 1);
   1.332 +by (strip_tac 1);
   1.333 +by (case_tac "x:B" 1);
   1.334 + by (dtac mk_disjoint_insert 1);
   1.335 + by (SELECT_GOAL(safe_tac HOL_cs)1);
   1.336 + by (rotate_tac ~1 1);
   1.337 + by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
   1.338 +by (rotate_tac ~1 1);
   1.339 +by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
   1.340  qed_spec_mp "card_mono";
     2.1 --- a/src/HOL/equalities.ML	Wed Mar 06 12:52:11 1996 +0100
     2.2 +++ b/src/HOL/equalities.ML	Wed Mar 06 13:57:07 1996 +0100
     2.3 @@ -13,24 +13,24 @@
     2.4  section "{}";
     2.5  
     2.6  goal Set.thy "{x.False} = {}";
     2.7 -by(fast_tac eq_cs 1);
     2.8 +by (fast_tac eq_cs 1);
     2.9  qed "Collect_False_empty";
    2.10  Addsimps [Collect_False_empty];
    2.11  
    2.12  goal Set.thy "(A <= {}) = (A = {})";
    2.13 -by(fast_tac eq_cs 1);
    2.14 +by (fast_tac eq_cs 1);
    2.15  qed "subset_empty";
    2.16  Addsimps [subset_empty];
    2.17  
    2.18  section ":";
    2.19  
    2.20  goal Set.thy "x ~: {}";
    2.21 -by(fast_tac set_cs 1);
    2.22 +by (fast_tac set_cs 1);
    2.23  qed "in_empty";
    2.24  Addsimps[in_empty];
    2.25  
    2.26  goal Set.thy "x : insert y A = (x=y | x:A)";
    2.27 -by(fast_tac set_cs 1);
    2.28 +by (fast_tac set_cs 1);
    2.29  qed "in_insert";
    2.30  Addsimps[in_insert];
    2.31  
    2.32 @@ -38,7 +38,7 @@
    2.33  
    2.34  (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
    2.35  goal Set.thy "insert a A = {a} Un A";
    2.36 -by(fast_tac eq_cs 1);
    2.37 +by (fast_tac eq_cs 1);
    2.38  qed "insert_is_Un";
    2.39  
    2.40  goal Set.thy "insert a A ~= {}";
    2.41 @@ -54,7 +54,7 @@
    2.42  qed "insert_absorb";
    2.43  
    2.44  goal Set.thy "insert x (insert x A) = insert x A";
    2.45 -by(fast_tac eq_cs 1);
    2.46 +by (fast_tac eq_cs 1);
    2.47  qed "insert_absorb2";
    2.48  Addsimps [insert_absorb2];
    2.49  
    2.50 @@ -65,8 +65,8 @@
    2.51  
    2.52  (* use new B rather than (A-{a}) to avoid infinite unfolding *)
    2.53  goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
    2.54 -by(res_inst_tac [("x","A-{a}")] exI 1);
    2.55 -by(fast_tac eq_cs 1);
    2.56 +by (res_inst_tac [("x","A-{a}")] exI 1);
    2.57 +by (fast_tac eq_cs 1);
    2.58  qed "mk_disjoint_insert";
    2.59  
    2.60  section "''";
    2.61 @@ -145,27 +145,27 @@
    2.62  qed "Un_assoc";
    2.63  
    2.64  goal Set.thy "{} Un B = B";
    2.65 -by(fast_tac eq_cs 1);
    2.66 +by (fast_tac eq_cs 1);
    2.67  qed "Un_empty_left";
    2.68  Addsimps[Un_empty_left];
    2.69  
    2.70  goal Set.thy "A Un {} = A";
    2.71 -by(fast_tac eq_cs 1);
    2.72 +by (fast_tac eq_cs 1);
    2.73  qed "Un_empty_right";
    2.74  Addsimps[Un_empty_right];
    2.75  
    2.76  goal Set.thy "UNIV Un B = UNIV";
    2.77 -by(fast_tac eq_cs 1);
    2.78 +by (fast_tac eq_cs 1);
    2.79  qed "Un_UNIV_left";
    2.80  Addsimps[Un_UNIV_left];
    2.81  
    2.82  goal Set.thy "A Un UNIV = UNIV";
    2.83 -by(fast_tac eq_cs 1);
    2.84 +by (fast_tac eq_cs 1);
    2.85  qed "Un_UNIV_right";
    2.86  Addsimps[Un_UNIV_right];
    2.87  
    2.88  goal Set.thy "insert a B Un C = insert a (B Un C)";
    2.89 -by(fast_tac eq_cs 1);
    2.90 +by (fast_tac eq_cs 1);
    2.91  qed "Un_insert_left";
    2.92  
    2.93  goal Set.thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
    2.94 @@ -437,7 +437,7 @@
    2.95  Addsimps[Diff_UNIV];
    2.96  
    2.97  goal Set.thy "!!x. x~:A ==> A - insert x B = A-B";
    2.98 -by(fast_tac eq_cs 1);
    2.99 +by (fast_tac eq_cs 1);
   2.100  qed "Diff_insert0";
   2.101  Addsimps [Diff_insert0];
   2.102  
   2.103 @@ -452,12 +452,12 @@
   2.104  qed "Diff_insert2";
   2.105  
   2.106  goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
   2.107 -by(simp_tac (!simpset setloop split_tac[expand_if]) 1);
   2.108 -by(fast_tac eq_cs 1);
   2.109 +by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
   2.110 +by (fast_tac eq_cs 1);
   2.111  qed "insert_Diff_if";
   2.112  
   2.113  goal Set.thy "!!x. x:B ==> insert x A - B = A-B";
   2.114 -by(fast_tac eq_cs 1);
   2.115 +by (fast_tac eq_cs 1);
   2.116  qed "insert_Diff1";
   2.117  Addsimps [insert_Diff1];
   2.118