Replaced fast_tac by Fast_tac (which uses default claset)
authorberghofe
Thu May 23 14:37:06 1996 +0200 (1996-05-23)
changeset 17606f41a494f3b1
parent 1759 a42d6c537f4a
child 1761 29e08d527ba1
Replaced fast_tac by Fast_tac (which uses default claset)
New rules are now also added to default claset.
src/HOL/Arith.ML
src/HOL/Finite.ML
src/HOL/Lfp.ML
src/HOL/List.ML
src/HOL/Nat.ML
src/HOL/RelPow.ML
src/HOL/Set.ML
src/HOL/Sexp.ML
src/HOL/Sum.ML
src/HOL/Trancl.ML
src/HOL/Univ.ML
src/HOL/WF.ML
src/HOL/mono.ML
src/HOL/subset.ML
     1.1 --- a/src/HOL/Arith.ML	Wed May 22 18:32:37 1996 +0200
     1.2 +++ b/src/HOL/Arith.ML	Thu May 23 14:37:06 1996 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4  by (etac rev_mp 1);
     1.5  by (nat_ind_tac "k" 1);
     1.6  by (Simp_tac 1);
     1.7 -by (fast_tac HOL_cs 1);
     1.8 +by (Fast_tac 1);
     1.9  val lemma = result();
    1.10  
    1.11  (* [| 0 < k; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *)
    1.12 @@ -233,7 +233,7 @@
    1.13  (*In ordinary notation: if 0<n and n<=m then m-n < m *)
    1.14  goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m";
    1.15  by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
    1.16 -by (fast_tac HOL_cs 1);
    1.17 +by (Fast_tac 1);
    1.18  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.19  by (ALLGOALS(asm_simp_tac(!simpset addsimps [diff_less_Suc])));
    1.20  qed "diff_less";
    1.21 @@ -321,7 +321,7 @@
    1.22  
    1.23  goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
    1.24  by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
    1.25 -by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o fast_tac HOL_cs));
    1.26 +by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o Fast_tac));
    1.27  qed "zero_induct_lemma";
    1.28  
    1.29  val prems = goal Arith.thy "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
    1.30 @@ -366,11 +366,13 @@
    1.31  
    1.32  val less_cs = set_cs addSEs [less_zeroE, less_SucE];
    1.33  
    1.34 +AddSEs [less_zeroE, less_SucE];
    1.35 +
    1.36  goal thy "!!k b. b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
    1.37  by (subgoal_tac "k mod 2 < 2" 1);
    1.38  by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
    1.39  by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
    1.40 -by (fast_tac less_cs 1);
    1.41 +by (Fast_tac 1);
    1.42  qed "mod2_cases";
    1.43  
    1.44  goal thy "Suc(Suc(m)) mod 2 = m mod 2";
    1.45 @@ -434,7 +436,7 @@
    1.46  by (etac rev_mp 1);
    1.47  by (nat_ind_tac "j" 1);
    1.48  by (ALLGOALS Asm_simp_tac);
    1.49 -by (fast_tac (HOL_cs addDs [Suc_lessD]) 1);
    1.50 +by (fast_tac (!claset addDs [Suc_lessD]) 1);
    1.51  qed "add_lessD1";
    1.52  
    1.53  goal Arith.thy "!!k::nat. m <= n ==> m <= n+k";
    1.54 @@ -450,7 +452,7 @@
    1.55  goal Arith.thy "m+k<=n --> m<=(n::nat)";
    1.56  by (nat_ind_tac "k" 1);
    1.57  by (ALLGOALS Asm_simp_tac);
    1.58 -by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
    1.59 +by (fast_tac (!claset addDs [Suc_leD]) 1);
    1.60  qed_spec_mp "add_leD1";
    1.61  
    1.62  goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
    1.63 @@ -486,7 +488,7 @@
    1.64  \     |] ==> f(i) <= (f(j)::nat)";
    1.65  by (cut_facts_tac [le] 1);
    1.66  by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
    1.67 -by (fast_tac (HOL_cs addSIs [lt_mono]) 1);
    1.68 +by (fast_tac (!claset addSIs [lt_mono]) 1);
    1.69  qed "less_mono_imp_le_mono";
    1.70  
    1.71  (*non-strict, in 1st argument*)
     2.1 --- a/src/HOL/Finite.ML	Wed May 22 18:32:37 1996 +0200
     2.2 +++ b/src/HOL/Finite.ML	Thu May 23 14:37:06 1996 +0200
     2.3 @@ -16,7 +16,7 @@
     2.4  qed "Fin_mono";
     2.5  
     2.6  goalw Finite.thy Fin.defs "Fin(A) <= Pow(A)";
     2.7 -by (fast_tac (set_cs addSIs [lfp_lowerbound]) 1);
     2.8 +by (fast_tac (!claset addSIs [lfp_lowerbound]) 1);
     2.9  qed "Fin_subset_Pow";
    2.10  
    2.11  (* A : Fin(B) ==> A <= B *)
    2.12 @@ -55,7 +55,7 @@
    2.13  qed "Fin_subset";
    2.14  
    2.15  goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";
    2.16 -by (fast_tac (set_cs addIs [Fin_UnI] addDs
    2.17 +by (fast_tac (!claset addIs [Fin_UnI] addDs
    2.18                  [Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
    2.19  qed "subset_Fin";
    2.20  Addsimps[subset_Fin];
    2.21 @@ -63,7 +63,7 @@
    2.22  goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)";
    2.23  by (stac insert_is_Un 1);
    2.24  by (Simp_tac 1);
    2.25 -by (fast_tac (set_cs addSIs Fin.intrs addDs [FinD]) 1);
    2.26 +by (fast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1);
    2.27  qed "insert_Fin";
    2.28  Addsimps[insert_Fin];
    2.29  
    2.30 @@ -163,7 +163,7 @@
    2.31  section "Finite cardinality -- 'card'";
    2.32  
    2.33  goal Set.thy "{f i |i. P i | i=n} = insert (f n) {f i|i. P i}";
    2.34 -by (fast_tac eq_cs 1);
    2.35 +by (Fast_tac 1);
    2.36  val Collect_conv_insert = result();
    2.37  
    2.38  goalw Finite.thy [card_def] "card {} = 0";
    2.39 @@ -197,7 +197,7 @@
    2.40  by (case_tac "? a. a:A" 1);
    2.41   by (res_inst_tac [("x","0")] exI 2);
    2.42   by (Simp_tac 2);
    2.43 - by (fast_tac eq_cs 2);
    2.44 + by (Fast_tac 2);
    2.45  by (etac exE 1);
    2.46  by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    2.47  by (rtac exI 1);
    2.48 @@ -212,7 +212,7 @@
    2.49    by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
    2.50    by (SELECT_GOAL(safe_tac eq_cs)1);
    2.51     by (subgoal_tac "x ~= f m" 1);
    2.52 -    by (fast_tac set_cs 2);
    2.53 +    by (Fast_tac 2);
    2.54     by (subgoal_tac "? k. f k = x & k<m" 1);
    2.55      by (best_tac set_cs 2);
    2.56     by (SELECT_GOAL(safe_tac HOL_cs)1);
    2.57 @@ -226,7 +226,7 @@
    2.58   by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
    2.59   by (SELECT_GOAL(safe_tac eq_cs)1);
    2.60    by (subgoal_tac "x ~= f m" 1);
    2.61 -   by (fast_tac set_cs 2);
    2.62 +   by (Fast_tac 2);
    2.63    by (subgoal_tac "? k. f k = x & k<m" 1);
    2.64     by (best_tac set_cs 2);
    2.65    by (SELECT_GOAL(safe_tac HOL_cs)1);
    2.66 @@ -237,7 +237,7 @@
    2.67  by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
    2.68  by (SELECT_GOAL(safe_tac eq_cs)1);
    2.69   by (subgoal_tac "x ~= f i" 1);
    2.70 -  by (fast_tac set_cs 2);
    2.71 +  by (Fast_tac 2);
    2.72   by (case_tac "x = f m" 1);
    2.73    by (res_inst_tac [("x","i")] exI 1);
    2.74    by (Asm_simp_tac 1);
    2.75 @@ -305,8 +305,8 @@
    2.76  by (Asm_simp_tac 1);
    2.77  by (rtac card_insert_disjoint 1);
    2.78  by (rtac (major RSN (2,finite_subset)) 1);
    2.79 -by (fast_tac set_cs 1);
    2.80 -by (fast_tac HOL_cs 1);
    2.81 +by (Fast_tac 1);
    2.82 +by (Fast_tac 1);
    2.83  by (asm_simp_tac (!simpset addsimps [major RS card_insert_disjoint]) 1);
    2.84  qed "card_insert";
    2.85  Addsimps [card_insert];
     3.1 --- a/src/HOL/Lfp.ML	Wed May 22 18:32:37 1996 +0200
     3.2 +++ b/src/HOL/Lfp.ML	Thu May 23 14:37:06 1996 +0200
     3.3 @@ -60,7 +60,7 @@
     3.4  goal Lfp.thy "!!f. [| mono f; f A <= A |] ==> lfp(f) <= A";
     3.5  by (rtac subsetI 1);
     3.6  by (EVERY[etac induct 1, atac 1, etac subsetD 1, rtac subsetD 1,
     3.7 -                atac 2, fast_tac (set_cs addSEs [monoD]) 1]);
     3.8 +                atac 2, fast_tac (!claset addSEs [monoD]) 1]);
     3.9  qed "Park_induct";
    3.10  
    3.11  (** Definition forms of lfp_Tarski and induct, to control unfolding **)
     4.1 --- a/src/HOL/List.ML	Wed May 22 18:32:37 1996 +0200
     4.2 +++ b/src/HOL/List.ML	Thu May 23 14:37:06 1996 +0200
     4.3 @@ -95,7 +95,7 @@
     4.4  goal List.thy "(Alls x:xs.P(x)) = (!x. x mem xs --> P(x))";
     4.5  by (list.induct_tac "xs" 1);
     4.6  by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
     4.7 -by (fast_tac HOL_cs 1);
     4.8 +by (Fast_tac 1);
     4.9  qed "list_all_mem_conv";
    4.10  
    4.11  
    4.12 @@ -106,13 +106,13 @@
    4.13  \                         (!y ys. xs=y#ys --> P(f y ys)))";
    4.14  by (list.induct_tac "xs" 1);
    4.15  by (ALLGOALS Asm_simp_tac);
    4.16 -by (fast_tac HOL_cs 1);
    4.17 +by (Fast_tac 1);
    4.18  qed "expand_list_case";
    4.19  
    4.20  goal List.thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
    4.21  by (list.induct_tac "xs" 1);
    4.22 -by (fast_tac HOL_cs 1);
    4.23 -by (fast_tac HOL_cs 1);
    4.24 +by (Fast_tac 1);
    4.25 +by (Fast_tac 1);
    4.26  bind_thm("list_eq_cases",
    4.27    impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
    4.28  
     5.1 --- a/src/HOL/Nat.ML	Wed May 22 18:32:37 1996 +0200
     5.2 +++ b/src/HOL/Nat.ML	Thu May 23 14:37:06 1996 +0200
     5.3 @@ -32,7 +32,7 @@
     5.4      "[| i: Nat;  P(Zero_Rep);   \
     5.5  \       !!j. [| j: Nat; P(j) |] ==> P(Suc_Rep(j)) |]  ==> P(i)";
     5.6  by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_induct) 1);
     5.7 -by (fast_tac (set_cs addIs prems) 1);
     5.8 +by (fast_tac (!claset addIs prems) 1);
     5.9  qed "Nat_induct";
    5.10  
    5.11  val prems = goalw Nat.thy [Zero_def,Suc_def]
    5.12 @@ -66,10 +66,10 @@
    5.13  val prems = goal Nat.thy 
    5.14      "[| n=0 ==> P;  !!x. n = Suc(x) ==> P |] ==> P";
    5.15  by (subgoal_tac "n=0 | (EX x. n = Suc(x))" 1);
    5.16 -by (fast_tac (HOL_cs addSEs prems) 1);
    5.17 +by (fast_tac (!claset addSEs prems) 1);
    5.18  by (nat_ind_tac "n" 1);
    5.19  by (rtac (refl RS disjI1) 1);
    5.20 -by (fast_tac HOL_cs 1);
    5.21 +by (Fast_tac 1);
    5.22  qed "natE";
    5.23  
    5.24  (*** Isomorphisms: Abs_Nat and Rep_Nat ***)
    5.25 @@ -128,18 +128,18 @@
    5.26  (*** nat_case -- the selection operator for nat ***)
    5.27  
    5.28  goalw Nat.thy [nat_case_def] "nat_case a f 0 = a";
    5.29 -by (fast_tac (set_cs addIs [select_equality] addEs [Zero_neq_Suc]) 1);
    5.30 +by (fast_tac (!claset addIs [select_equality] addEs [Zero_neq_Suc]) 1);
    5.31  qed "nat_case_0";
    5.32  
    5.33  goalw Nat.thy [nat_case_def] "nat_case a f (Suc k) = f(k)";
    5.34 -by (fast_tac (set_cs addIs [select_equality] 
    5.35 +by (fast_tac (!claset addIs [select_equality] 
    5.36                         addEs [make_elim Suc_inject, Suc_neq_Zero]) 1);
    5.37  qed "nat_case_Suc";
    5.38  
    5.39  (** Introduction rules for 'pred_nat' **)
    5.40  
    5.41  goalw Nat.thy [pred_nat_def] "(n, Suc(n)) : pred_nat";
    5.42 -by (fast_tac set_cs 1);
    5.43 +by (Fast_tac 1);
    5.44  qed "pred_natI";
    5.45  
    5.46  val major::prems = goalw Nat.thy [pred_nat_def]
    5.47 @@ -152,9 +152,9 @@
    5.48  goalw Nat.thy [wf_def] "wf(pred_nat)";
    5.49  by (strip_tac 1);
    5.50  by (nat_ind_tac "x" 1);
    5.51 -by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, 
    5.52 +by (fast_tac (!claset addSEs [mp, pred_natE, Pair_inject, 
    5.53                               make_elim Suc_inject]) 2);
    5.54 -by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, Zero_neq_Suc]) 1);
    5.55 +by (fast_tac (!claset addSEs [mp, pred_natE, Pair_inject, Zero_neq_Suc]) 1);
    5.56  qed "wf_pred_nat";
    5.57  
    5.58  
    5.59 @@ -231,7 +231,7 @@
    5.60  (** Elimination properties **)
    5.61  
    5.62  val prems = goalw Nat.thy [less_def] "n<m ==> ~ m<(n::nat)";
    5.63 -by (fast_tac (HOL_cs addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
    5.64 +by (fast_tac (!claset addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
    5.65  qed "less_not_sym";
    5.66  
    5.67  (* [| n(m; m(n |] ==> R *)
    5.68 @@ -246,7 +246,7 @@
    5.69  bind_thm ("less_irrefl", (less_not_refl RS notE));
    5.70  
    5.71  goal Nat.thy "!!m. n<m ==> m ~= (n::nat)";
    5.72 -by (fast_tac (HOL_cs addEs [less_irrefl]) 1);
    5.73 +by (fast_tac (!claset addEs [less_irrefl]) 1);
    5.74  qed "less_not_refl2";
    5.75  
    5.76  
    5.77 @@ -274,13 +274,13 @@
    5.78      "[| m < Suc(n);  m<n ==> P;  m=n ==> P |] ==> P";
    5.79  by (rtac (major RS lessE) 1);
    5.80  by (rtac eq 1);
    5.81 -by (fast_tac (HOL_cs addSDs [Suc_inject]) 1);
    5.82 +by (fast_tac (!claset addSDs [Suc_inject]) 1);
    5.83  by (rtac less 1);
    5.84 -by (fast_tac (HOL_cs addSDs [Suc_inject]) 1);
    5.85 +by (fast_tac (!claset addSDs [Suc_inject]) 1);
    5.86  qed "less_SucE";
    5.87  
    5.88  goal Nat.thy "(m < Suc(n)) = (m < n | m = n)";
    5.89 -by (fast_tac (HOL_cs addSIs [lessI]
    5.90 +by (fast_tac (!claset addSIs [lessI]
    5.91                       addEs  [less_trans, less_SucE]) 1);
    5.92  qed "less_Suc_eq";
    5.93  
    5.94 @@ -306,7 +306,7 @@
    5.95  by (nat_ind_tac "n" 1);
    5.96  by (rtac impI 1);
    5.97  by (etac less_zeroE 1);
    5.98 -by (fast_tac (HOL_cs addSIs [lessI RS less_SucI]
    5.99 +by (fast_tac (!claset addSIs [lessI RS less_SucI]
   5.100                       addSDs [Suc_inject]
   5.101                       addEs  [less_trans, lessE]) 1);
   5.102  qed "Suc_lessD";
   5.103 @@ -328,11 +328,11 @@
   5.104  
   5.105  val prems = goal Nat.thy "m<n ==> Suc(m) < Suc(n)";
   5.106  by (subgoal_tac "m<n --> Suc(m) < Suc(n)" 1);
   5.107 -by (fast_tac (HOL_cs addIs prems) 1);
   5.108 +by (fast_tac (!claset addIs prems) 1);
   5.109  by (nat_ind_tac "n" 1);
   5.110  by (rtac impI 1);
   5.111  by (etac less_zeroE 1);
   5.112 -by (fast_tac (HOL_cs addSIs [lessI]
   5.113 +by (fast_tac (!claset addSIs [lessI]
   5.114                       addSDs [Suc_inject]
   5.115                       addEs  [less_trans, lessE]) 1);
   5.116  qed "Suc_mono";
   5.117 @@ -353,7 +353,7 @@
   5.118  Addsimps [Suc_less_eq];
   5.119  
   5.120  goal Nat.thy "~(Suc(n) < n)";
   5.121 -by (fast_tac (HOL_cs addEs [Suc_lessD RS less_irrefl]) 1);
   5.122 +by (fast_tac (!claset addEs [Suc_lessD RS less_irrefl]) 1);
   5.123  qed "not_Suc_n_less_n";
   5.124  Addsimps [not_Suc_n_less_n];
   5.125  
   5.126 @@ -361,7 +361,7 @@
   5.127  by (nat_ind_tac "k" 1);
   5.128  by (ALLGOALS (asm_simp_tac (!simpset)));
   5.129  by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   5.130 -by (fast_tac (HOL_cs addDs [Suc_lessD]) 1);
   5.131 +by (fast_tac (!claset addDs [Suc_lessD]) 1);
   5.132  qed_spec_mp "less_trans_Suc";
   5.133  
   5.134  (*"Less than" is a linear ordering*)
   5.135 @@ -370,7 +370,7 @@
   5.136  by (nat_ind_tac "n" 1);
   5.137  by (rtac (refl RS disjI1 RS disjI2) 1);
   5.138  by (rtac (zero_less_Suc RS disjI1) 1);
   5.139 -by (fast_tac (HOL_cs addIs [lessI, Suc_mono, less_SucI] addEs [lessE]) 1);
   5.140 +by (fast_tac (!claset addIs [lessI, Suc_mono, less_SucI] addEs [lessE]) 1);
   5.141  qed "less_linear";
   5.142  
   5.143  qed_goal "nat_less_cases" Nat.thy 
   5.144 @@ -439,40 +439,40 @@
   5.145  val leE = make_elim leD;
   5.146  
   5.147  goal Nat.thy "(~n<m) = (m<=(n::nat))";
   5.148 -by (fast_tac (HOL_cs addIs [leI] addEs [leE]) 1);
   5.149 +by (fast_tac (!claset addIs [leI] addEs [leE]) 1);
   5.150  qed "not_less_iff_le";
   5.151  
   5.152  goalw Nat.thy [le_def] "!!m. ~ m <= n ==> n<(m::nat)";
   5.153 -by (fast_tac HOL_cs 1);
   5.154 +by (Fast_tac 1);
   5.155  qed "not_leE";
   5.156  
   5.157  goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n";
   5.158  by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   5.159 -by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1);
   5.160 +by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
   5.161  qed "lessD";
   5.162  
   5.163  goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
   5.164  by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   5.165 -by (fast_tac HOL_cs 1);
   5.166 +by (Fast_tac 1);
   5.167  qed "Suc_leD";
   5.168  
   5.169  goalw Nat.thy [le_def] "!!m. m <= n ==> m <= Suc n";
   5.170 -by (fast_tac (HOL_cs addDs [Suc_lessD]) 1);
   5.171 +by (fast_tac (!claset addDs [Suc_lessD]) 1);
   5.172  qed "le_SucI";
   5.173  Addsimps[le_SucI];
   5.174  
   5.175  goalw Nat.thy [le_def] "!!m. m < n ==> m <= (n::nat)";
   5.176 -by (fast_tac (HOL_cs addEs [less_asym]) 1);
   5.177 +by (fast_tac (!claset addEs [less_asym]) 1);
   5.178  qed "less_imp_le";
   5.179  
   5.180  goalw Nat.thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)";
   5.181  by (cut_facts_tac [less_linear] 1);
   5.182 -by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1);
   5.183 +by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
   5.184  qed "le_imp_less_or_eq";
   5.185  
   5.186  goalw Nat.thy [le_def] "!!m. m<n | m=n ==> m <=(n::nat)";
   5.187  by (cut_facts_tac [less_linear] 1);
   5.188 -by (fast_tac (HOL_cs addEs [less_irrefl,less_asym]) 1);
   5.189 +by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
   5.190  by (flexflex_tac);
   5.191  qed "less_or_eq_imp_le";
   5.192  
   5.193 @@ -486,22 +486,22 @@
   5.194  
   5.195  val prems = goal Nat.thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
   5.196  by (dtac le_imp_less_or_eq 1);
   5.197 -by (fast_tac (HOL_cs addIs [less_trans]) 1);
   5.198 +by (fast_tac (!claset addIs [less_trans]) 1);
   5.199  qed "le_less_trans";
   5.200  
   5.201  goal Nat.thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)";
   5.202  by (dtac le_imp_less_or_eq 1);
   5.203 -by (fast_tac (HOL_cs addIs [less_trans]) 1);
   5.204 +by (fast_tac (!claset addIs [less_trans]) 1);
   5.205  qed "less_le_trans";
   5.206  
   5.207  goal Nat.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)";
   5.208  by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
   5.209 -          rtac less_or_eq_imp_le, fast_tac (HOL_cs addIs [less_trans])]);
   5.210 +          rtac less_or_eq_imp_le, fast_tac (!claset addIs [less_trans])]);
   5.211  qed "le_trans";
   5.212  
   5.213  val prems = goal Nat.thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
   5.214  by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
   5.215 -          fast_tac (HOL_cs addEs [less_irrefl,less_asym])]);
   5.216 +          fast_tac (!claset addEs [less_irrefl,less_asym])]);
   5.217  qed "le_anti_sym";
   5.218  
   5.219  goal Nat.thy "(Suc(n) <= Suc(m)) = (n <= m)";
   5.220 @@ -516,9 +516,9 @@
   5.221  val [prem1,prem2] = goalw Nat.thy [Least_def]
   5.222      "[| P(k);  !!x. x<k ==> ~P(x) |] ==> (LEAST x.P(x)) = k";
   5.223  by (rtac select_equality 1);
   5.224 -by (fast_tac (HOL_cs addSIs [prem1,prem2]) 1);
   5.225 +by (fast_tac (!claset addSIs [prem1,prem2]) 1);
   5.226  by (cut_facts_tac [less_linear] 1);
   5.227 -by (fast_tac (HOL_cs addSIs [prem1] addSDs [prem2]) 1);
   5.228 +by (fast_tac (!claset addSIs [prem1] addSDs [prem2]) 1);
   5.229  qed "Least_equality";
   5.230  
   5.231  val [prem] = goal Nat.thy "P(k) ==> P(LEAST x.P(x))";
   5.232 @@ -529,7 +529,7 @@
   5.233  by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
   5.234  by (assume_tac 1);
   5.235  by (assume_tac 2);
   5.236 -by (fast_tac HOL_cs 1);
   5.237 +by (Fast_tac 1);
   5.238  qed "LeastI";
   5.239  
   5.240  (*Proof is almost identical to the one above!*)
   5.241 @@ -541,7 +541,7 @@
   5.242  by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
   5.243  by (assume_tac 1);
   5.244  by (rtac le_refl 2);
   5.245 -by (fast_tac (HOL_cs addIs [less_imp_le,le_trans]) 1);
   5.246 +by (fast_tac (!claset addIs [less_imp_le,le_trans]) 1);
   5.247  qed "Least_le";
   5.248  
   5.249  val [prem] = goal Nat.thy "k < (LEAST x.P(x)) ==> ~P(k)";
   5.250 @@ -558,19 +558,19 @@
   5.251  	fold_goals_tac [Least_def],
   5.252  	safe_tac (HOL_cs addSEs [LeastI]),
   5.253  	res_inst_tac [("n","j")] natE 1,
   5.254 -	fast_tac HOL_cs 1,
   5.255 -	fast_tac (HOL_cs addDs [Suc_less_SucD] addDs [not_less_Least]) 1,	
   5.256 +	Fast_tac 1,
   5.257 +	fast_tac (!claset addDs [Suc_less_SucD] addDs [not_less_Least]) 1,	
   5.258  	res_inst_tac [("n","k")] natE 1,
   5.259 -	fast_tac HOL_cs 1,
   5.260 +	Fast_tac 1,
   5.261  	hyp_subst_tac 1,
   5.262  	rewtac Least_def,
   5.263  	rtac (select_equality RS arg_cong RS sym) 1,
   5.264  	safe_tac HOL_cs,
   5.265  	dtac Suc_mono 1,
   5.266 -	fast_tac HOL_cs 1,
   5.267 +	Fast_tac 1,
   5.268  	cut_facts_tac [less_linear] 1,
   5.269  	safe_tac HOL_cs,
   5.270  	atac 2,
   5.271 -	fast_tac HOL_cs 2,
   5.272 +	Fast_tac 2,
   5.273  	dtac Suc_mono 1,
   5.274 -	fast_tac HOL_cs 1]);
   5.275 +	Fast_tac 1]);
     6.1 --- a/src/HOL/RelPow.ML	Wed May 22 18:32:37 1996 +0200
     6.2 +++ b/src/HOL/RelPow.ML	Thu May 23 14:37:06 1996 +0200
     6.3 @@ -20,15 +20,15 @@
     6.4  
     6.5  goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
     6.6  by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
     6.7 -by (fast_tac comp_cs 1);
     6.8 +by (Fast_tac 1);
     6.9  qed "rel_pow_Suc_I";
    6.10  
    6.11  goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
    6.12  by (nat_ind_tac "n" 1);
    6.13  by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    6.14 -by (fast_tac comp_cs 1);
    6.15 +by (Fast_tac 1);
    6.16  by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    6.17 -by (fast_tac comp_cs 1);
    6.18 +by (Fast_tac 1);
    6.19  qed_spec_mp "rel_pow_Suc_I2";
    6.20  
    6.21  goal RelPow.thy "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
    6.22 @@ -39,7 +39,7 @@
    6.23    "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
    6.24  by (cut_facts_tac [major] 1);
    6.25  by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    6.26 -by (fast_tac (comp_cs addIs [minor]) 1);
    6.27 +by (fast_tac (!claset addIs [minor]) 1);
    6.28  qed "rel_pow_Suc_E";
    6.29  
    6.30  val [p1,p2,p3] = goal RelPow.thy
    6.31 @@ -57,8 +57,8 @@
    6.32  
    6.33  goal RelPow.thy "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
    6.34  by (nat_ind_tac "n" 1);
    6.35 -by (fast_tac (HOL_cs addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
    6.36 -by (fast_tac (HOL_cs addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
    6.37 +by (fast_tac (!claset addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
    6.38 +by (fast_tac (!claset addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
    6.39  qed_spec_mp "rel_pow_Suc_D2";
    6.40  
    6.41  val [p1,p2,p3] = goal RelPow.thy
    6.42 @@ -80,13 +80,13 @@
    6.43  goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)";
    6.44  by (split_all_tac 1);
    6.45  by (etac rtrancl_induct 1);
    6.46 -by (ALLGOALS (fast_tac (rel_cs addIs [rel_pow_0_I,rel_pow_Suc_I])));
    6.47 +by (ALLGOALS (fast_tac (!claset addIs [rel_pow_0_I,rel_pow_Suc_I])));
    6.48  qed "rtrancl_imp_UN_rel_pow";
    6.49  
    6.50  goal RelPow.thy "!y. (x,y):R^n --> (x,y):R^*";
    6.51  by (nat_ind_tac "n" 1);
    6.52 -by (fast_tac (HOL_cs addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
    6.53 -by (fast_tac (trancl_cs addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);
    6.54 +by (fast_tac (!claset addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
    6.55 +by (fast_tac (!claset addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);
    6.56  val lemma = result() RS spec RS mp;
    6.57  
    6.58  goal RelPow.thy "!!p. p:R^n ==> p:R^*";
    6.59 @@ -95,5 +95,5 @@
    6.60  qed "rel_pow_imp_rtrancl";
    6.61  
    6.62  goal RelPow.thy "R^* = (UN n. R^n)";
    6.63 -by (fast_tac (eq_cs addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
    6.64 +by (fast_tac (!claset addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
    6.65  qed "rtrancl_is_UN_rel_pow";
     7.1 --- a/src/HOL/Set.ML	Wed May 22 18:32:37 1996 +0200
     7.2 +++ b/src/HOL/Set.ML	Thu May 23 14:37:06 1996 +0200
     7.3 @@ -188,7 +188,7 @@
     7.4  val ComplE = make_elim ComplD;
     7.5  
     7.6  qed_goal "Compl_iff" Set.thy "(c : Compl(A)) = (c~:A)"
     7.7 - (fn _ => [ (fast_tac (HOL_cs addSIs [ComplI] addSEs [ComplE]) 1) ]);
     7.8 + (fn _ => [ (fast_tac (!claset addSIs [ComplI] addSEs [ComplE]) 1) ]);
     7.9  
    7.10  
    7.11  section "Binary union -- Un";
    7.12 @@ -215,7 +215,7 @@
    7.13  qed "UnE";
    7.14  
    7.15  qed_goal "Un_iff" Set.thy "(c : A Un B) = (c:A | c:B)"
    7.16 - (fn _ => [ (fast_tac (HOL_cs addSIs [UnCI] addSEs [UnE]) 1) ]);
    7.17 + (fn _ => [ (fast_tac (!claset addSIs [UnCI] addSEs [UnE]) 1) ]);
    7.18  
    7.19  
    7.20  section "Binary intersection -- Int";
    7.21 @@ -241,7 +241,7 @@
    7.22  qed "IntE";
    7.23  
    7.24  qed_goal "Int_iff" Set.thy "(c : A Int B) = (c:A & c:B)"
    7.25 - (fn _ => [ (fast_tac (HOL_cs addSIs [IntI] addSEs [IntE]) 1) ]);
    7.26 + (fn _ => [ (fast_tac (!claset addSIs [IntI] addSEs [IntE]) 1) ]);
    7.27  
    7.28  
    7.29  section "Set difference";
    7.30 @@ -266,7 +266,7 @@
    7.31      (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]);
    7.32  
    7.33  qed_goal "Diff_iff" Set.thy "(c : A-B) = (c:A & c~:B)"
    7.34 - (fn _ => [ (fast_tac (HOL_cs addSIs [DiffI] addSEs [DiffE]) 1) ]);
    7.35 + (fn _ => [ (fast_tac (!claset addSIs [DiffI] addSEs [DiffE]) 1) ]);
    7.36  
    7.37  section "The empty set -- {}";
    7.38  
    7.39 @@ -286,7 +286,7 @@
    7.40    [ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]);
    7.41  
    7.42  qed_goal "empty_iff" Set.thy "(c : {}) = False"
    7.43 - (fn _ => [ (fast_tac (HOL_cs addSEs [emptyE]) 1) ]);
    7.44 + (fn _ => [ (fast_tac (!claset addSEs [emptyE]) 1) ]);
    7.45  
    7.46  
    7.47  section "Augmenting a set -- insert";
    7.48 @@ -304,7 +304,7 @@
    7.49      (REPEAT (eresolve_tac (prems @ [CollectE]) 1)) ]);
    7.50  
    7.51  qed_goal "insert_iff" Set.thy "a : insert b A = (a=b | a:A)"
    7.52 - (fn _ => [fast_tac (HOL_cs addIs [insertI1,insertI2] addSEs [insertE]) 1]);
    7.53 + (fn _ => [fast_tac (!claset addIs [insertI1,insertI2] addSEs [insertE]) 1]);
    7.54  
    7.55  (*Classical introduction rule*)
    7.56  qed_goal "insertCI" Set.thy "(a~:B ==> a=b) ==> a: insert b B"
    7.57 @@ -323,7 +323,7 @@
    7.58      (REPEAT (eresolve_tac (prems @ [emptyE]) 1)) ]);
    7.59  
    7.60  goalw Set.thy [insert_def] "!!a. b : {a} ==> b=a";
    7.61 -by (fast_tac (HOL_cs addSEs [emptyE,CollectE,UnE]) 1);
    7.62 +by (fast_tac (!claset addSEs [emptyE,CollectE,UnE]) 1);
    7.63  qed "singletonD";
    7.64  
    7.65  val singletonE = make_elim singletonD;
     8.1 --- a/src/HOL/Sexp.ML	Wed May 22 18:32:37 1996 +0200
     8.2 +++ b/src/HOL/Sexp.ML	Thu May 23 14:37:06 1996 +0200
     8.3 @@ -16,19 +16,24 @@
     8.4                     Numb_neq_Scons, Numb_neq_Leaf,
     8.5                     Scons_neq_Leaf, Scons_neq_Numb];
     8.6  
     8.7 +AddSDs [Leaf_inject, Numb_inject, Scons_inject];
     8.8 +AddSEs [Leaf_neq_Scons, Leaf_neq_Numb,
     8.9 +                   Numb_neq_Scons, Numb_neq_Leaf,
    8.10 +                   Scons_neq_Leaf, Scons_neq_Numb];
    8.11 +
    8.12  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
    8.13  by (resolve_tac [select_equality] 1);
    8.14 -by (ALLGOALS (fast_tac sexp_free_cs));
    8.15 +by (ALLGOALS (Fast_tac));
    8.16  qed "sexp_case_Leaf";
    8.17  
    8.18  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
    8.19  by (resolve_tac [select_equality] 1);
    8.20 -by (ALLGOALS (fast_tac sexp_free_cs));
    8.21 +by (ALLGOALS (Fast_tac));
    8.22  qed "sexp_case_Numb";
    8.23  
    8.24  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N";
    8.25  by (resolve_tac [select_equality] 1);
    8.26 -by (ALLGOALS (fast_tac sexp_free_cs));
    8.27 +by (ALLGOALS (Fast_tac));
    8.28  qed "sexp_case_Scons";
    8.29  
    8.30  
    8.31 @@ -46,21 +51,23 @@
    8.32  
    8.33  val sexp_cs = set_cs addIs sexp.intrs@[SigmaI, uprodI];
    8.34  
    8.35 +AddIs (sexp.intrs@[SigmaI, uprodI]);
    8.36 +
    8.37  goal Sexp.thy "range(Leaf) <= sexp";
    8.38 -by (fast_tac sexp_cs 1);
    8.39 +by (Fast_tac 1);
    8.40  qed "range_Leaf_subset_sexp";
    8.41  
    8.42  val [major] = goal Sexp.thy "M$N : sexp ==> M: sexp & N: sexp";
    8.43  by (rtac (major RS setup_induction) 1);
    8.44  by (etac sexp.induct 1);
    8.45  by (ALLGOALS 
    8.46 -    (fast_tac (set_cs addSEs [Scons_neq_Leaf,Scons_neq_Numb,Scons_inject])));
    8.47 +    (fast_tac (!claset addSEs [Scons_neq_Leaf,Scons_neq_Numb,Scons_inject])));
    8.48  qed "Scons_D";
    8.49  
    8.50  (** Introduction rules for 'pred_sexp' **)
    8.51  
    8.52  goalw Sexp.thy [pred_sexp_def] "pred_sexp <= sexp Times sexp";
    8.53 -by (fast_tac sexp_cs 1);
    8.54 +by (Fast_tac 1);
    8.55  qed "pred_sexp_subset_Sigma";
    8.56  
    8.57  (* (a,b) : pred_sexp^+ ==> a : sexp *)
    8.58 @@ -71,12 +78,12 @@
    8.59  
    8.60  val prems = goalw Sexp.thy [pred_sexp_def]
    8.61      "[| M: sexp;  N: sexp |] ==> (M, M$N) : pred_sexp";
    8.62 -by (fast_tac (set_cs addIs prems) 1);
    8.63 +by (fast_tac (!claset addIs prems) 1);
    8.64  qed "pred_sexpI1";
    8.65  
    8.66  val prems = goalw Sexp.thy [pred_sexp_def]
    8.67      "[| M: sexp;  N: sexp |] ==> (N, M$N) : pred_sexp";
    8.68 -by (fast_tac (set_cs addIs prems) 1);
    8.69 +by (fast_tac (!claset addIs prems) 1);
    8.70  qed "pred_sexpI2";
    8.71  
    8.72  (*Combinations involving transitivity and the rules above*)
    8.73 @@ -102,9 +109,9 @@
    8.74  goal Sexp.thy "wf(pred_sexp)";
    8.75  by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
    8.76  by (etac sexp.induct 1);
    8.77 -by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Scons_inject]) 3);
    8.78 -by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Numb_neq_Scons]) 2);
    8.79 -by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Leaf_neq_Scons]) 1);
    8.80 +by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Scons_inject]) 3);
    8.81 +by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Numb_neq_Scons]) 2);
    8.82 +by (fast_tac (!claset addSEs [mp, pred_sexpE, Pair_inject, Leaf_neq_Scons]) 1);
    8.83  qed "wf_pred_sexp";
    8.84  
    8.85  (*** sexp_rec -- by wf recursion on pred_sexp ***)
     9.1 --- a/src/HOL/Sum.ML	Wed May 22 18:32:37 1996 +0200
     9.2 +++ b/src/HOL/Sum.ML	Thu May 23 14:37:06 1996 +0200
     9.3 @@ -56,12 +56,12 @@
     9.4  
     9.5  val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
     9.6  by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
     9.7 -by (fast_tac HOL_cs 1);
     9.8 +by (Fast_tac 1);
     9.9  qed "Inl_Rep_inject";
    9.10  
    9.11  val [major] = goalw Sum.thy [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
    9.12  by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
    9.13 -by (fast_tac HOL_cs 1);
    9.14 +by (Fast_tac 1);
    9.15  qed "Inr_Rep_inject";
    9.16  
    9.17  goalw Sum.thy [Inl_def] "inj(Inl)";
    9.18 @@ -81,11 +81,11 @@
    9.19  val Inr_inject = inj_Inr RS injD;
    9.20  
    9.21  goal Sum.thy "(Inl(x)=Inl(y)) = (x=y)";
    9.22 -by (fast_tac (HOL_cs addSEs [Inl_inject]) 1);
    9.23 +by (fast_tac (!claset addSEs [Inl_inject]) 1);
    9.24  qed "Inl_eq";
    9.25  
    9.26  goal Sum.thy "(Inr(x)=Inr(y)) = (x=y)";
    9.27 -by (fast_tac (HOL_cs addSEs [Inr_inject]) 1);
    9.28 +by (fast_tac (!claset addSEs [Inr_inject]) 1);
    9.29  qed "Inr_eq";
    9.30  
    9.31  (*** Rules for the disjoint sum of two SETS ***)
    9.32 @@ -117,15 +117,19 @@
    9.33                      addSEs [plusE, Inl_neq_Inr, Inr_neq_Inl]
    9.34                      addSDs [Inl_inject, Inr_inject];
    9.35  
    9.36 +AddSIs [InlI, InrI]; 
    9.37 +AddSEs [plusE, Inl_neq_Inr, Inr_neq_Inl];
    9.38 +AddSDs [Inl_inject, Inr_inject];
    9.39 +
    9.40  
    9.41  (** sum_case -- the selection operator for sums **)
    9.42  
    9.43  goalw Sum.thy [sum_case_def] "sum_case f g (Inl x) = f(x)";
    9.44 -by (fast_tac (sum_cs addIs [select_equality]) 1);
    9.45 +by (fast_tac (!claset addIs [select_equality]) 1);
    9.46  qed "sum_case_Inl";
    9.47  
    9.48  goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)";
    9.49 -by (fast_tac (sum_cs addIs [select_equality]) 1);
    9.50 +by (fast_tac (!claset addIs [select_equality]) 1);
    9.51  qed "sum_case_Inr";
    9.52  
    9.53  (** Exhaustion rule for sums -- a degenerate form of induction **)
    9.54 @@ -151,10 +155,10 @@
    9.55  by (rtac sumE 1);
    9.56  by (etac ssubst 1);
    9.57  by (stac sum_case_Inl 1);
    9.58 -by (fast_tac (set_cs addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
    9.59 +by (fast_tac (!claset addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
    9.60  by (etac ssubst 1);
    9.61  by (stac sum_case_Inr 1);
    9.62 -by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
    9.63 +by (fast_tac (!claset addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
    9.64  qed "expand_sum_case";
    9.65  
    9.66  Addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq,  sum_case_Inl, sum_case_Inr];
    9.67 @@ -171,7 +175,7 @@
    9.68  
    9.69  goalw Sum.thy [Part_def]
    9.70      "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part A h";
    9.71 -by (fast_tac set_cs 1);
    9.72 +by (Fast_tac 1);
    9.73  qed "Part_eqI";
    9.74  
    9.75  val PartI = refl RSN (2,Part_eqI);
    9.76 @@ -190,7 +194,7 @@
    9.77  qed "Part_subset";
    9.78  
    9.79  goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h";
    9.80 -by (fast_tac (set_cs addSIs [PartI] addSEs [PartE]) 1);
    9.81 +by (fast_tac (!claset addSIs [PartI] addSEs [PartE]) 1);
    9.82  qed "Part_mono";
    9.83  
    9.84  val basic_monos = basic_monos @ [Part_mono];
    9.85 @@ -200,14 +204,14 @@
    9.86  qed "PartD1";
    9.87  
    9.88  goal Sum.thy "Part A (%x.x) = A";
    9.89 -by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
    9.90 +by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
    9.91  qed "Part_id";
    9.92  
    9.93  goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
    9.94 -by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
    9.95 +by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
    9.96  qed "Part_Int";
    9.97  
    9.98  (*For inductive definitions*)
    9.99  goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
   9.100 -by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
   9.101 +by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
   9.102  qed "Part_Collect";
    10.1 --- a/src/HOL/Trancl.ML	Wed May 22 18:32:37 1996 +0200
    10.2 +++ b/src/HOL/Trancl.ML	Thu May 23 14:37:06 1996 +0200
    10.3 @@ -20,14 +20,14 @@
    10.4  (*Reflexivity of rtrancl*)
    10.5  goal Trancl.thy "(a,a) : r^*";
    10.6  by (stac rtrancl_unfold 1);
    10.7 -by (fast_tac rel_cs 1);
    10.8 +by (Fast_tac 1);
    10.9  qed "rtrancl_refl";
   10.10  
   10.11  (*Closure under composition with r*)
   10.12  val prems = goal Trancl.thy
   10.13      "[| (a,b) : r^*;  (b,c) : r |] ==> (a,c) : r^*";
   10.14  by (stac rtrancl_unfold 1);
   10.15 -by (fast_tac (rel_cs addIs prems) 1);
   10.16 +by (fast_tac (!claset addIs prems) 1);
   10.17  qed "rtrancl_into_rtrancl";
   10.18  
   10.19  (*rtrancl of r contains r*)
   10.20 @@ -49,7 +49,7 @@
   10.21  \     !!x y z.[| P((x,y)); (x,y): r^*; (y,z): r |]  ==>  P((x,z)) |] \
   10.22  \  ==>  P((a,b))";
   10.23  by (rtac ([rtrancl_def, rtrancl_fun_mono, major] MRS def_induct) 1);
   10.24 -by (fast_tac (rel_cs addIs prems) 1);
   10.25 +by (fast_tac (!claset addIs prems) 1);
   10.26  qed "rtrancl_full_induct";
   10.27  
   10.28  (*nice induction rule*)
   10.29 @@ -61,11 +61,11 @@
   10.30  (*by induction on this formula*)
   10.31  by (subgoal_tac "! y. (a::'a,b) = (a,y) --> P(y)" 1);
   10.32  (*now solve first subgoal: this formula is sufficient*)
   10.33 -by (fast_tac HOL_cs 1);
   10.34 +by (Fast_tac 1);
   10.35  (*now do the induction*)
   10.36  by (resolve_tac [major RS rtrancl_full_induct] 1);
   10.37 -by (fast_tac (rel_cs addIs prems) 1);
   10.38 -by (fast_tac (rel_cs addIs prems) 1);
   10.39 +by (fast_tac (!claset addIs prems) 1);
   10.40 +by (fast_tac (!claset addIs prems) 1);
   10.41  qed "rtrancl_induct";
   10.42  
   10.43  bind_thm
   10.44 @@ -77,7 +77,7 @@
   10.45  goalw Trancl.thy [trans_def] "trans(r^*)";
   10.46  by (safe_tac HOL_cs);
   10.47  by (eres_inst_tac [("b","z")] rtrancl_induct 1);
   10.48 -by (ALLGOALS(fast_tac (HOL_cs addIs [rtrancl_into_rtrancl])));
   10.49 +by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
   10.50  qed "trans_rtrancl";
   10.51  
   10.52  bind_thm ("rtrancl_trans", trans_rtrancl RS transD);
   10.53 @@ -90,8 +90,8 @@
   10.54  \    |] ==> P";
   10.55  by (subgoal_tac "(a::'a) = b  | (? y. (a,y) : r^* & (y,b) : r)" 1);
   10.56  by (rtac (major RS rtrancl_induct) 2);
   10.57 -by (fast_tac (set_cs addIs prems) 2);
   10.58 -by (fast_tac (set_cs addIs prems) 2);
   10.59 +by (fast_tac (!claset addIs prems) 2);
   10.60 +by (fast_tac (!claset addIs prems) 2);
   10.61  by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
   10.62  qed "rtranclE";
   10.63  
   10.64 @@ -107,7 +107,7 @@
   10.65  by (rtac iffI 1);
   10.66  by (etac rtrancl_induct 1);
   10.67  by (rtac rtrancl_refl 1);
   10.68 -by (fast_tac (HOL_cs addEs [rtrancl_trans]) 1);
   10.69 +by (fast_tac (!claset addEs [rtrancl_trans]) 1);
   10.70  by (etac r_into_rtrancl 1);
   10.71  qed "rtrancl_idemp";
   10.72  Addsimps [rtrancl_idemp];
   10.73 @@ -121,7 +121,7 @@
   10.74  by (dtac rtrancl_mono 1);
   10.75  by (dtac rtrancl_mono 1);
   10.76  by (Asm_full_simp_tac 1);
   10.77 -by (fast_tac eq_cs 1);
   10.78 +by (Fast_tac 1);
   10.79  qed "rtrancl_subset";
   10.80  
   10.81  goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
   10.82 @@ -138,14 +138,14 @@
   10.83  by (rtac converseI 1);
   10.84  by (etac rtrancl_induct 1);
   10.85  by (rtac rtrancl_refl 1);
   10.86 -by (fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
   10.87 +by (fast_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 1);
   10.88  qed "rtrancl_converseD";
   10.89  
   10.90  goal Trancl.thy "!!r. (x,y) : converse(r^*) ==> (x,y) : (converse r)^*";
   10.91  by (dtac converseD 1);
   10.92  by (etac rtrancl_induct 1);
   10.93  by (rtac rtrancl_refl 1);
   10.94 -by (fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
   10.95 +by (fast_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 1);
   10.96  qed "rtrancl_converseI";
   10.97  
   10.98  goal Trancl.thy "(converse r)^* = converse(r^*)";
   10.99 @@ -161,7 +161,7 @@
  10.100  \     ==> P(a)";
  10.101  br ((major RS converseI RS rtrancl_converseI) RS rtrancl_induct) 1;
  10.102   brs prems 1;
  10.103 -by(fast_tac (HOL_cs addIs prems addSEs[converseD]addSDs[rtrancl_converseD])1);
  10.104 +by(fast_tac (!claset addIs prems addSEs[converseD]addSDs[rtrancl_converseD])1);
  10.105  qed "converse_rtrancl_induct";
  10.106  
  10.107  val prems = goal Trancl.thy
  10.108 @@ -221,9 +221,9 @@
  10.109  (*by induction on this formula*)
  10.110  by (subgoal_tac "ALL z. (y,z) : r --> P(z)" 1);
  10.111  (*now solve first subgoal: this formula is sufficient*)
  10.112 -by (fast_tac HOL_cs 1);
  10.113 +by (Fast_tac 1);
  10.114  by (etac rtrancl_induct 1);
  10.115 -by (ALLGOALS (fast_tac (set_cs addIs (rtrancl_into_trancl1::prems))));
  10.116 +by (ALLGOALS (fast_tac (!claset addIs (rtrancl_into_trancl1::prems))));
  10.117  qed "trancl_induct";
  10.118  
  10.119  (*elimination of r^+ -- NOT an induction rule*)
  10.120 @@ -236,8 +236,8 @@
  10.121  by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
  10.122  by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
  10.123  by (etac rtranclE 1);
  10.124 -by (fast_tac rel_cs 1);
  10.125 -by (fast_tac (rel_cs addSIs [rtrancl_into_trancl1]) 1);
  10.126 +by (Fast_tac 1);
  10.127 +by (fast_tac (!claset addSIs [rtrancl_into_trancl1]) 1);
  10.128  qed "tranclE";
  10.129  
  10.130  (*Transitivity of r^+.
  10.131 @@ -264,15 +264,15 @@
  10.132  by (cut_facts_tac prems 1);
  10.133  by (rtac (major RS rtrancl_induct) 1);
  10.134  by (rtac (refl RS disjI1) 1);
  10.135 -by (fast_tac (rel_cs addSEs [SigmaE2]) 1);
  10.136 +by (fast_tac (!claset addSEs [SigmaE2]) 1);
  10.137  val lemma = result();
  10.138  
  10.139  goalw Trancl.thy [trancl_def]
  10.140      "!!r. r <= A Times A ==> r^+ <= A Times A";
  10.141 -by (fast_tac (rel_cs addSDs [lemma]) 1);
  10.142 +by (fast_tac (!claset addSDs [lemma]) 1);
  10.143  qed "trancl_subset_Sigma";
  10.144  
  10.145  (* Don't add r_into_rtrancl: it messes up the proofs in Lambda *)
  10.146  val trancl_cs = rel_cs addIs [rtrancl_refl];
  10.147  
  10.148 -
  10.149 +AddIs [rtrancl_refl];
    11.1 --- a/src/HOL/Univ.ML	Wed May 22 18:32:37 1996 +0200
    11.2 +++ b/src/HOL/Univ.ML	Thu May 23 14:37:06 1996 +0200
    11.3 @@ -69,12 +69,12 @@
    11.4  (*** Introduction rules for Node ***)
    11.5  
    11.6  goalw Univ.thy [Node_def] "(%k. 0,a) : Node";
    11.7 -by (fast_tac set_cs 1);
    11.8 +by (Fast_tac 1);
    11.9  qed "Node_K0_I";
   11.10  
   11.11  goalw Univ.thy [Node_def,Push_def]
   11.12      "!!p. p: Node ==> apfst (Push i) p : Node";
   11.13 -by (fast_tac (set_cs addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
   11.14 +by (fast_tac (!claset addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
   11.15  qed "Node_Push_I";
   11.16  
   11.17  
   11.18 @@ -100,7 +100,7 @@
   11.19  (** Atomic nodes **)
   11.20  
   11.21  goalw Univ.thy [Atom_def, inj_def] "inj(Atom)";
   11.22 -by (fast_tac (prod_cs addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1);
   11.23 +by (fast_tac (!claset addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1);
   11.24  qed "inj_Atom";
   11.25  val Atom_inject = inj_Atom RS injD;
   11.26  
   11.27 @@ -139,13 +139,13 @@
   11.28  
   11.29  val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> M<=M'";
   11.30  by (cut_facts_tac [major] 1);
   11.31 -by (fast_tac (set_cs addSDs [Suc_inject]
   11.32 +by (fast_tac (!claset addSDs [Suc_inject]
   11.33                       addSEs [Push_Node_inject, Zero_neq_Suc]) 1);
   11.34  qed "Scons_inject_lemma1";
   11.35  
   11.36  val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> N<=N'";
   11.37  by (cut_facts_tac [major] 1);
   11.38 -by (fast_tac (set_cs addSDs [Suc_inject]
   11.39 +by (fast_tac (!claset addSDs [Suc_inject]
   11.40                       addSEs [Push_Node_inject, Suc_neq_Zero]) 1);
   11.41  qed "Scons_inject_lemma2";
   11.42  
   11.43 @@ -167,11 +167,11 @@
   11.44  
   11.45  (*rewrite rules*)
   11.46  goal Univ.thy "(Atom(a)=Atom(b)) = (a=b)";
   11.47 -by (fast_tac (HOL_cs addSEs [Atom_inject]) 1);
   11.48 +by (fast_tac (!claset addSEs [Atom_inject]) 1);
   11.49  qed "Atom_Atom_eq";
   11.50  
   11.51  goal Univ.thy "(M$N = M'$N') = (M=M' & N=N')";
   11.52 -by (fast_tac (HOL_cs addSEs [Scons_inject]) 1);
   11.53 +by (fast_tac (!claset addSEs [Scons_inject]) 1);
   11.54  qed "Scons_Scons_eq";
   11.55  
   11.56  (*** Distinctness involving Leaf and Numb ***)
   11.57 @@ -323,11 +323,11 @@
   11.58  (*** Disjoint Sum ***)
   11.59  
   11.60  goalw Univ.thy [usum_def] "!!M. M:A ==> In0(M) : A<+>B";
   11.61 -by (fast_tac set_cs 1);
   11.62 +by (Fast_tac 1);
   11.63  qed "usum_In0I";
   11.64  
   11.65  goalw Univ.thy [usum_def] "!!N. N:B ==> In1(N) : A<+>B";
   11.66 -by (fast_tac set_cs 1);
   11.67 +by (Fast_tac 1);
   11.68  qed "usum_In1I";
   11.69  
   11.70  val major::prems = goalw Univ.thy [usum_def]
   11.71 @@ -364,12 +364,12 @@
   11.72  (*** proving equality of sets and functions using ntrunc ***)
   11.73  
   11.74  goalw Univ.thy [ntrunc_def] "ntrunc k M <= M";
   11.75 -by (fast_tac set_cs 1);
   11.76 +by (Fast_tac 1);
   11.77  qed "ntrunc_subsetI";
   11.78  
   11.79  val [major] = goalw Univ.thy [ntrunc_def]
   11.80      "(!!k. ntrunc k M <= N) ==> M<=N";
   11.81 -by (fast_tac (set_cs addIs [less_add_Suc1, less_add_Suc2, 
   11.82 +by (fast_tac (!claset addIs [less_add_Suc1, less_add_Suc2, 
   11.83                              major RS subsetD]) 1);
   11.84  qed "ntrunc_subsetD";
   11.85  
   11.86 @@ -391,15 +391,15 @@
   11.87  (*** Monotonicity ***)
   11.88  
   11.89  goalw Univ.thy [uprod_def] "!!A B. [| A<=A';  B<=B' |] ==> A<*>B <= A'<*>B'";
   11.90 -by (fast_tac set_cs 1);
   11.91 +by (Fast_tac 1);
   11.92  qed "uprod_mono";
   11.93  
   11.94  goalw Univ.thy [usum_def] "!!A B. [| A<=A';  B<=B' |] ==> A<+>B <= A'<+>B'";
   11.95 -by (fast_tac set_cs 1);
   11.96 +by (Fast_tac 1);
   11.97  qed "usum_mono";
   11.98  
   11.99  goalw Univ.thy [Scons_def] "!!M N. [| M<=M';  N<=N' |] ==> M$N <= M'$N'";
  11.100 -by (fast_tac set_cs 1);
  11.101 +by (Fast_tac 1);
  11.102  qed "Scons_mono";
  11.103  
  11.104  goalw Univ.thy [In0_def] "!!M N. M<=N ==> In0(M) <= In0(N)";
  11.105 @@ -414,31 +414,31 @@
  11.106  (*** Split and Case ***)
  11.107  
  11.108  goalw Univ.thy [Split_def] "Split c (M$N) = c M N";
  11.109 -by (fast_tac (set_cs addIs [select_equality] addEs [Scons_inject]) 1);
  11.110 +by (fast_tac (!claset addIs [select_equality] addEs [Scons_inject]) 1);
  11.111  qed "Split";
  11.112  
  11.113  goalw Univ.thy [Case_def] "Case c d (In0 M) = c(M)";
  11.114 -by (fast_tac (set_cs addIs [select_equality] 
  11.115 +by (fast_tac (!claset addIs [select_equality] 
  11.116                       addEs [make_elim In0_inject, In0_neq_In1]) 1);
  11.117  qed "Case_In0";
  11.118  
  11.119  goalw Univ.thy [Case_def] "Case c d (In1 N) = d(N)";
  11.120 -by (fast_tac (set_cs addIs [select_equality] 
  11.121 +by (fast_tac (!claset addIs [select_equality] 
  11.122                       addEs [make_elim In1_inject, In1_neq_In0]) 1);
  11.123  qed "Case_In1";
  11.124  
  11.125  (**** UN x. B(x) rules ****)
  11.126  
  11.127  goalw Univ.thy [ntrunc_def] "ntrunc k (UN x.f(x)) = (UN x. ntrunc k (f x))";
  11.128 -by (fast_tac (set_cs addIs [equalityI]) 1);
  11.129 +by (fast_tac (!claset addIs [equalityI]) 1);
  11.130  qed "ntrunc_UN1";
  11.131  
  11.132  goalw Univ.thy [Scons_def] "(UN x.f(x)) $ M = (UN x. f(x) $ M)";
  11.133 -by (fast_tac (set_cs addIs [equalityI]) 1);
  11.134 +by (fast_tac (!claset addIs [equalityI]) 1);
  11.135  qed "Scons_UN1_x";
  11.136  
  11.137  goalw Univ.thy [Scons_def] "M $ (UN x.f(x)) = (UN x. M $ f(x))";
  11.138 -by (fast_tac (set_cs addIs [equalityI]) 1);
  11.139 +by (fast_tac (!claset addIs [equalityI]) 1);
  11.140  qed "Scons_UN1_y";
  11.141  
  11.142  goalw Univ.thy [In0_def] "In0(UN x.f(x)) = (UN x. In0(f(x)))";
  11.143 @@ -453,7 +453,7 @@
  11.144  (*** Equality : the diagonal relation ***)
  11.145  
  11.146  goalw Univ.thy [diag_def] "!!a A. [| a=b;  a:A |] ==> (a,b) : diag(A)";
  11.147 -by (fast_tac set_cs 1);
  11.148 +by (Fast_tac 1);
  11.149  qed "diag_eqI";
  11.150  
  11.151  val diagI = refl RS diag_eqI |> standard;
  11.152 @@ -471,7 +471,7 @@
  11.153  
  11.154  goalw Univ.thy [dprod_def]
  11.155      "!!r s. [| (M,M'):r;  (N,N'):s |] ==> (M$N, M'$N') : r<**>s";
  11.156 -by (fast_tac prod_cs 1);
  11.157 +by (Fast_tac 1);
  11.158  qed "dprodI";
  11.159  
  11.160  (*The general elimination rule*)
  11.161 @@ -488,11 +488,11 @@
  11.162  (*** Equality for Disjoint Sum ***)
  11.163  
  11.164  goalw Univ.thy [dsum_def]  "!!r. (M,M'):r ==> (In0(M), In0(M')) : r<++>s";
  11.165 -by (fast_tac prod_cs 1);
  11.166 +by (Fast_tac 1);
  11.167  qed "dsum_In0I";
  11.168  
  11.169  goalw Univ.thy [dsum_def]  "!!r. (N,N'):s ==> (In1(N), In1(N')) : r<++>s";
  11.170 -by (fast_tac prod_cs 1);
  11.171 +by (Fast_tac 1);
  11.172  qed "dsum_In1I";
  11.173  
  11.174  val major::prems = goalw Univ.thy [dsum_def]
  11.175 @@ -511,26 +511,29 @@
  11.176              addIs  [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I]
  11.177              addSEs [diagE, uprodE, dprodE, usumE, dsumE];
  11.178  
  11.179 +AddSIs [diagI, uprodI, dprodI];
  11.180 +AddIs  [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I];
  11.181 +AddSEs [diagE, uprodE, dprodE, usumE, dsumE];
  11.182  
  11.183  (*** Monotonicity ***)
  11.184  
  11.185  goal Univ.thy "!!r s. [| r<=r';  s<=s' |] ==> r<**>s <= r'<**>s'";
  11.186 -by (fast_tac univ_cs 1);
  11.187 +by (Fast_tac 1);
  11.188  qed "dprod_mono";
  11.189  
  11.190  goal Univ.thy "!!r s. [| r<=r';  s<=s' |] ==> r<++>s <= r'<++>s'";
  11.191 -by (fast_tac univ_cs 1);
  11.192 +by (Fast_tac 1);
  11.193  qed "dsum_mono";
  11.194  
  11.195  
  11.196  (*** Bounding theorems ***)
  11.197  
  11.198  goal Univ.thy "diag(A) <= A Times A";
  11.199 -by (fast_tac univ_cs 1);
  11.200 +by (Fast_tac 1);
  11.201  qed "diag_subset_Sigma";
  11.202  
  11.203  goal Univ.thy "((A Times B) <**> (C Times D)) <= (A<*>C) Times (B<*>D)";
  11.204 -by (fast_tac univ_cs 1);
  11.205 +by (Fast_tac 1);
  11.206  qed "dprod_Sigma";
  11.207  
  11.208  val dprod_subset_Sigma = [dprod_mono, dprod_Sigma] MRS subset_trans |>standard;
  11.209 @@ -540,11 +543,11 @@
  11.210      "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))";
  11.211  by (safe_tac univ_cs);
  11.212  by (stac Split 1);
  11.213 -by (fast_tac univ_cs 1);
  11.214 +by (Fast_tac 1);
  11.215  qed "dprod_subset_Sigma2";
  11.216  
  11.217  goal Univ.thy "(A Times B <++> C Times D) <= (A<+>C) Times (B<+>D)";
  11.218 -by (fast_tac univ_cs 1);
  11.219 +by (Fast_tac 1);
  11.220  qed "dsum_Sigma";
  11.221  
  11.222  val dsum_subset_Sigma = [dsum_mono, dsum_Sigma] MRS subset_trans |> standard;
  11.223 @@ -553,16 +556,16 @@
  11.224  (*** Domain ***)
  11.225  
  11.226  goal Univ.thy "fst `` diag(A) = A";
  11.227 -by (fast_tac (prod_cs addIs [equalityI, diagI] addSEs [diagE]) 1);
  11.228 +by (fast_tac (!claset addIs [equalityI, diagI] addSEs [diagE]) 1);
  11.229  qed "fst_image_diag";
  11.230  
  11.231  goal Univ.thy "fst `` (r<**>s) = (fst``r) <*> (fst``s)";
  11.232 -by (fast_tac (prod_cs addIs [equalityI, uprodI, dprodI]
  11.233 +by (fast_tac (!claset addIs [equalityI, uprodI, dprodI]
  11.234                       addSEs [uprodE, dprodE]) 1);
  11.235  qed "fst_image_dprod";
  11.236  
  11.237  goal Univ.thy "fst `` (r<++>s) = (fst``r) <+> (fst``s)";
  11.238 -by (fast_tac (prod_cs addIs [equalityI, usum_In0I, usum_In1I, 
  11.239 +by (fast_tac (!claset addIs [equalityI, usum_In0I, usum_In1I, 
  11.240                               dsum_In0I, dsum_In1I]
  11.241                       addSEs [usumE, dsumE]) 1);
  11.242  qed "fst_image_dsum";
    12.1 --- a/src/HOL/WF.ML	Wed May 22 18:32:37 1996 +0200
    12.2 +++ b/src/HOL/WF.ML	Thu May 23 14:37:06 1996 +0200
    12.3 @@ -27,7 +27,7 @@
    12.4  \       !!x.[| ! y. (y,x): r --> P(y) |] ==> P(x) \
    12.5  \    |]  ==>  P(a)";
    12.6  by (rtac (major RS spec RS mp RS spec) 1);
    12.7 -by (fast_tac (HOL_cs addEs prems) 1);
    12.8 +by (fast_tac (!claset addEs prems) 1);
    12.9  qed "wf_induct";
   12.10  
   12.11  (*Perform induction on i, then prove the wf(r) subgoal using prems. *)
   12.12 @@ -38,9 +38,9 @@
   12.13  
   12.14  val prems = goal WF.thy "[| wf(r);  (a,x):r;  (x,a):r |] ==> P";
   12.15  by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1);
   12.16 -by (fast_tac (HOL_cs addIs prems) 1);
   12.17 +by (fast_tac (!claset addIs prems) 1);
   12.18  by (wf_ind_tac "a" prems 1);
   12.19 -by (fast_tac set_cs 1);
   12.20 +by (Fast_tac 1);
   12.21  qed "wf_asym";
   12.22  
   12.23  val prems = goal WF.thy "[| wf(r);  (a,a): r |] ==> P";
   12.24 @@ -58,8 +58,8 @@
   12.25  by (res_inst_tac [("a","x")] (prem RS wf_induct) 1);
   12.26  by (rtac (impI RS allI) 1);
   12.27  by (etac tranclE 1);
   12.28 -by (fast_tac HOL_cs 1);
   12.29 -by (fast_tac HOL_cs 1);
   12.30 +by (Fast_tac 1);
   12.31 +by (Fast_tac 1);
   12.32  qed "wf_trancl";
   12.33  
   12.34  
    13.1 --- a/src/HOL/mono.ML	Wed May 22 18:32:37 1996 +0200
    13.2 +++ b/src/HOL/mono.ML	Thu May 23 14:37:06 1996 +0200
    13.3 @@ -7,58 +7,58 @@
    13.4  *)
    13.5  
    13.6  goal Set.thy "!!A B. A<=B ==> f``A <= f``B";
    13.7 -by (fast_tac set_cs 1);
    13.8 +by (Fast_tac 1);
    13.9  qed "image_mono";
   13.10  
   13.11  goal Set.thy "!!A B. A<=B ==> Pow(A) <= Pow(B)";
   13.12 -by (fast_tac set_cs 1);
   13.13 +by (Fast_tac 1);
   13.14  qed "Pow_mono";
   13.15  
   13.16  goal Set.thy "!!A B. A<=B ==> Union(A) <= Union(B)";
   13.17 -by (fast_tac set_cs 1);
   13.18 +by (Fast_tac 1);
   13.19  qed "Union_mono";
   13.20  
   13.21  goal Set.thy "!!A B. B<=A ==> Inter(A) <= Inter(B)";
   13.22 -by (fast_tac set_cs 1);
   13.23 +by (Fast_tac 1);
   13.24  qed "Inter_anti_mono";
   13.25  
   13.26  val prems = goal Set.thy
   13.27      "[| A<=B;  !!x. x:A ==> f(x)<=g(x) |] ==> \
   13.28  \    (UN x:A. f(x)) <= (UN x:B. g(x))";
   13.29 -by (fast_tac (set_cs addIs (prems RL [subsetD])) 1);
   13.30 +by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
   13.31  qed "UN_mono";
   13.32  
   13.33  val [prem] = goal Set.thy
   13.34      "[| !!x. f(x)<=g(x) |] ==> (UN x. f(x)) <= (UN x. g(x))";
   13.35 -by (fast_tac (set_cs addIs [prem RS subsetD]) 1);
   13.36 +by (fast_tac (!claset addIs [prem RS subsetD]) 1);
   13.37  qed "UN1_mono";
   13.38  
   13.39  val prems = goal Set.thy
   13.40      "[| B<=A;  !!x. x:A ==> f(x)<=g(x) |] ==> \
   13.41  \    (INT x:A. f(x)) <= (INT x:A. g(x))";
   13.42 -by (fast_tac (set_cs addIs (prems RL [subsetD])) 1);
   13.43 +by (fast_tac (!claset addIs (prems RL [subsetD])) 1);
   13.44  qed "INT_anti_mono";
   13.45  
   13.46  (*The inclusion is POSITIVE! *)
   13.47  val [prem] = goal Set.thy
   13.48      "[| !!x. f(x)<=g(x) |] ==> (INT x. f(x)) <= (INT x. g(x))";
   13.49 -by (fast_tac (set_cs addIs [prem RS subsetD]) 1);
   13.50 +by (fast_tac (!claset addIs [prem RS subsetD]) 1);
   13.51  qed "INT1_mono";
   13.52  
   13.53  goal Set.thy "!!A B. [| A<=C;  B<=D |] ==> A Un B <= C Un D";
   13.54 -by (fast_tac set_cs 1);
   13.55 +by (Fast_tac 1);
   13.56  qed "Un_mono";
   13.57  
   13.58  goal Set.thy "!!A B. [| A<=C;  B<=D |] ==> A Int B <= C Int D";
   13.59 -by (fast_tac set_cs 1);
   13.60 +by (Fast_tac 1);
   13.61  qed "Int_mono";
   13.62  
   13.63  goal Set.thy "!!A::'a set. [| A<=C;  D<=B |] ==> A-B <= C-D";
   13.64 -by (fast_tac set_cs 1);
   13.65 +by (Fast_tac 1);
   13.66  qed "Diff_mono";
   13.67  
   13.68  goal Set.thy "!!A B. A<=B ==> Compl(B) <= Compl(A)";
   13.69 -by (fast_tac set_cs 1);
   13.70 +by (Fast_tac 1);
   13.71  qed "Compl_anti_mono";
   13.72  
   13.73  (** Monotonicity of implications.  For inductive definitions **)
   13.74 @@ -70,15 +70,15 @@
   13.75  qed "in_mono";
   13.76  
   13.77  goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
   13.78 -by (fast_tac HOL_cs 1);
   13.79 +by (Fast_tac 1);
   13.80  qed "conj_mono";
   13.81  
   13.82  goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
   13.83 -by (fast_tac HOL_cs 1);
   13.84 +by (Fast_tac 1);
   13.85  qed "disj_mono";
   13.86  
   13.87  goal HOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
   13.88 -by (fast_tac HOL_cs 1);
   13.89 +by (Fast_tac 1);
   13.90  qed "imp_mono";
   13.91  
   13.92  goal HOL.thy "P-->P";
   13.93 @@ -88,24 +88,24 @@
   13.94  
   13.95  val [PQimp] = goal HOL.thy
   13.96      "[| !!x. P(x) --> Q(x) |] ==> (EX x.P(x)) --> (EX x.Q(x))";
   13.97 -by (fast_tac (HOL_cs addIs [PQimp RS mp]) 1);
   13.98 +by (fast_tac (!claset addIs [PQimp RS mp]) 1);
   13.99  qed "ex_mono";
  13.100  
  13.101  val [PQimp] = goal HOL.thy
  13.102      "[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))";
  13.103 -by (fast_tac (HOL_cs addIs [PQimp RS mp]) 1);
  13.104 +by (fast_tac (!claset addIs [PQimp RS mp]) 1);
  13.105  qed "all_mono";
  13.106  
  13.107  val [PQimp] = goal Set.thy
  13.108      "[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)";
  13.109 -by (fast_tac (set_cs addIs [PQimp RS mp]) 1);
  13.110 +by (fast_tac (!claset addIs [PQimp RS mp]) 1);
  13.111  qed "Collect_mono";
  13.112  
  13.113  (*Used in indrule.ML*)
  13.114  val [subs,PQimp] = goal Set.thy
  13.115      "[| A<=B;  !!x. x:A ==> P(x) --> Q(x) \
  13.116  \    |] ==> A Int Collect(P) <= B Int Collect(Q)";
  13.117 -by (fast_tac (set_cs addIs [subs RS subsetD, PQimp RS mp]) 1);
  13.118 +by (fast_tac (!claset addIs [subs RS subsetD, PQimp RS mp]) 1);
  13.119  qed "Int_Collect_mono";
  13.120  
  13.121  (*Used in intr_elim.ML and in individual datatype definitions*)
    14.1 --- a/src/HOL/subset.ML	Wed May 22 18:32:37 1996 +0200
    14.2 +++ b/src/HOL/subset.ML	Thu May 23 14:37:06 1996 +0200
    14.3 @@ -13,11 +13,11 @@
    14.4   (fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]);
    14.5  
    14.6  goal Set.thy "!!x. x ~: A ==> (A <= insert x B) = (A <= B)";
    14.7 -by (fast_tac set_cs 1);
    14.8 +by (Fast_tac 1);
    14.9  qed "subset_insert";
   14.10  
   14.11  qed_goal "subset_empty_iff" Set.thy "(A<={}) = (A={})"
   14.12 - (fn _=> [ (fast_tac (set_cs addIs [equalityI]) 1) ]);
   14.13 + (fn _=> [ (fast_tac (!claset addIs [equalityI]) 1) ]);
   14.14  
   14.15  (*** Big Union -- least upper bound of a set  ***)
   14.16