Classical tactics now use default claset.
authorberghofe
Tue Jul 30 17:33:26 1996 +0200 (1996-07-30)
changeset 1894c2c8279d40f0
parent 1893 fa58f4a06f21
child 1895 92b30c4829bf
Classical tactics now use default claset.
src/HOL/IOA/ABP/Correctness.ML
src/HOL/IOA/ABP/Lemmas.ML
src/HOL/IOA/NTP/Correctness.ML
src/HOL/IOA/NTP/Impl.ML
src/HOL/IOA/NTP/Lemmas.ML
src/HOL/IOA/NTP/Multiset.ML
src/HOL/IOA/meta_theory/IOA.ML
src/HOL/IOA/meta_theory/Option.ML
src/HOL/IOA/meta_theory/Solve.ML
src/HOL/Integ/Bin.ML
src/HOL/Integ/Equiv.ML
src/HOL/Integ/Integ.ML
src/HOL/Lex/Auto.ML
src/HOL/Lex/AutoChopper.ML
src/HOL/Lex/Prefix.ML
     1.1 --- a/src/HOL/IOA/ABP/Correctness.ML	Mon Jul 29 18:31:39 1996 +0200
     1.2 +++ b/src/HOL/IOA/ABP/Correctness.ML	Tue Jul 30 17:33:26 1996 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  open Impl; open Impl_finite;
     1.5  
     1.6  goal Abschannel.thy "(? x.x=P & Q(x)) = Q(P)";
     1.7 -by (fast_tac HOL_cs 1);
     1.8 +by (Fast_tac 1);
     1.9  qed"exis_elim";
    1.10  
    1.11  Delsimps [split_paired_All];
    1.12 @@ -47,7 +47,7 @@
    1.13  goal Correctness.thy "(reduce(l)=[]) = (l=[])";  
    1.14   by (rtac iffI 1);
    1.15   by (subgoal_tac "(l~=[]) --> (reduce(l)~=[])" 1);
    1.16 - by (fast_tac HOL_cs 1); 
    1.17 + by (Fast_tac 1); 
    1.18   by (List.list.induct_tac "l" 1);
    1.19   by (Simp_tac 1);
    1.20   by (Simp_tac 1);
    1.21 @@ -139,7 +139,7 @@
    1.22  by (case_tac "list=[]" 1);
    1.23   by (asm_full_simp_tac (!simpset addsimps [reverse_Nil,reverse_Cons]) 1);
    1.24  by (rtac (expand_if RS ssubst) 1);
    1.25 - by (fast_tac HOL_cs 1);
    1.26 + by (Fast_tac 1);
    1.27   by (rtac impI 1);
    1.28  by (Simp_tac 1);
    1.29  by (cut_inst_tac [("l","list")] cons_not_nil 1);
    1.30 @@ -230,7 +230,7 @@
    1.31  by (TRY(
    1.32     (rtac conjI 1) THEN
    1.33  (* start states *)
    1.34 -   (fast_tac set_cs 1)));
    1.35 +   (Fast_tac 1)));
    1.36  (* main-part *)
    1.37  by (REPEAT (rtac allI 1));
    1.38  by (rtac imp_conj_lemma 1);
    1.39 @@ -246,7 +246,7 @@
    1.40  by (TRY(
    1.41     (rtac conjI 1) THEN
    1.42   (* start states *)
    1.43 -   (fast_tac set_cs 1)));
    1.44 +   (Fast_tac 1)));
    1.45  (* main-part *)
    1.46  by (REPEAT (rtac allI 1));
    1.47  by (rtac imp_conj_lemma 1);
    1.48 @@ -261,7 +261,7 @@
    1.49  by (TRY(
    1.50     (rtac conjI 1) THEN
    1.51  (* start states *)
    1.52 -   (fast_tac set_cs 1)));
    1.53 +   (Fast_tac 1)));
    1.54  (* main-part *)
    1.55  by (REPEAT (rtac allI 1));
    1.56  by (rtac imp_conj_lemma 1);
     2.1 --- a/src/HOL/IOA/ABP/Lemmas.ML	Mon Jul 29 18:31:39 1996 +0200
     2.2 +++ b/src/HOL/IOA/ABP/Lemmas.ML	Tue Jul 30 17:33:26 1996 +0200
     2.3 @@ -8,22 +8,22 @@
     2.4  (* Logic *)
     2.5  
     2.6  val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
     2.7 -  by(fast_tac (HOL_cs addDs prems) 1);
     2.8 +  by(fast_tac (!claset addDs prems) 1);
     2.9  qed "imp_conj_lemma";
    2.10  
    2.11  goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)";
    2.12 -by (fast_tac HOL_cs 1);
    2.13 +by (Fast_tac 1);
    2.14  val and_de_morgan_and_absorbe = result();
    2.15  
    2.16  goal HOL.thy "(if C then A else B) --> (A|B)";
    2.17  by (rtac (expand_if RS ssubst) 1);
    2.18 -by (fast_tac HOL_cs 1);
    2.19 +by (Fast_tac 1);
    2.20  val bool_if_impl_or = result();
    2.21  
    2.22  (* Sets *)
    2.23  
    2.24  val set_lemmas =
    2.25 -   map (fn s => prove_goal Set.thy s (fn _ => [fast_tac set_cs 1]))
    2.26 +   map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1]))
    2.27          ["f(x) : (UN x. {f(x)})",
    2.28           "f x y : (UN x y. {f x y})",
    2.29           "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})",
    2.30 @@ -33,11 +33,11 @@
    2.31     namely for Intersections and the empty list (compatibility of IOA!)  *)
    2.32  goal Set.thy "(UN b.{x.x=f(b)})= (UN b.{f(b)})"; 
    2.33   by (rtac set_ext 1);
    2.34 - by (fast_tac set_cs 1);
    2.35 + by (Fast_tac 1);
    2.36  val singleton_set =result();
    2.37  
    2.38  goal HOL.thy "((A|B)=False) = ((~A)&(~B))";
    2.39 - by (fast_tac HOL_cs 1);
    2.40 + by (Fast_tac 1);
    2.41  val de_morgan = result();
    2.42  
    2.43  (* Lists *)
    2.44 @@ -53,5 +53,5 @@
    2.45  goal List.thy "l ~= [] --> (? x xs. l = (x#xs))";
    2.46   by (List.list.induct_tac "l" 1);
    2.47   by (simp_tac list_ss 1);
    2.48 - by (fast_tac HOL_cs 1);
    2.49 + by (Fast_tac 1);
    2.50  qed"cons_not_nil";
     3.1 --- a/src/HOL/IOA/NTP/Correctness.ML	Mon Jul 29 18:31:39 1996 +0200
     3.2 +++ b/src/HOL/IOA/NTP/Correctness.ML	Tue Jul 30 17:33:26 1996 +0200
     3.3 @@ -106,7 +106,7 @@
     3.4  by(case_tac "sq(sen(s))=[]" 1);
     3.5  
     3.6  by(asm_full_simp_tac ss' 1);
     3.7 -by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1);
     3.8 +by(fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
     3.9  
    3.10  by(case_tac "m = hd(sq(sen(s)))" 1);
    3.11  
    3.12 @@ -114,7 +114,7 @@
    3.13                       [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
    3.14  
    3.15  by(Asm_full_simp_tac 1);
    3.16 -by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1);
    3.17 +by(fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
    3.18  
    3.19  by(Asm_full_simp_tac 1);
    3.20  qed"ntp_correct";
     4.1 --- a/src/HOL/IOA/NTP/Impl.ML	Mon Jul 29 18:31:39 1996 +0200
     4.2 +++ b/src/HOL/IOA/NTP/Impl.ML	Tue Jul 30 17:33:26 1996 +0200
     4.3 @@ -182,14 +182,14 @@
     4.4    by (forward_tac [rewrite_rule [Impl.inv1_def]
     4.5                                  (inv1 RS invariantE) RS conjunct1] 1);
     4.6    by (tac2 1);
     4.7 -  by (fast_tac (HOL_cs addDs [add_leD1,leD]) 1);
     4.8 +  by (fast_tac (!claset addDs [add_leD1,leD]) 1);
     4.9  
    4.10    (* 3 *)
    4.11    by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1);
    4.12  
    4.13    by (tac2 1);
    4.14    by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]);
    4.15 -  by (fast_tac (HOL_cs addDs [add_leD1,leD]) 1);
    4.16 +  by (fast_tac (!claset addDs [add_leD1,leD]) 1);
    4.17  
    4.18    (* 2 *)
    4.19    by (tac2 1);
    4.20 @@ -245,7 +245,7 @@
    4.21    (* 7 *)
    4.22    by (tac3 1);
    4.23    by (tac_ren 1);
    4.24 -  by (fast_tac HOL_cs 1);
    4.25 +  by (Fast_tac 1);
    4.26  
    4.27    (* 6 - 3 *)
    4.28  
     5.1 --- a/src/HOL/IOA/NTP/Lemmas.ML	Mon Jul 29 18:31:39 1996 +0200
     5.2 +++ b/src/HOL/IOA/NTP/Lemmas.ML	Tue Jul 30 17:33:26 1996 +0200
     5.3 @@ -10,43 +10,43 @@
     5.4  
     5.5  (* Logic *)
     5.6  val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
     5.7 -  by(fast_tac (HOL_cs addDs prems) 1);
     5.8 +  by(fast_tac (!claset addDs prems) 1);
     5.9  qed "imp_conj_lemma";
    5.10  
    5.11  goal HOL.thy "(P --> (? x. Q(x))) = (? x. P --> Q(x))";
    5.12 -  by(fast_tac HOL_cs 1);
    5.13 +  by(Fast_tac 1);
    5.14  qed "imp_ex_equiv";
    5.15  
    5.16  goal HOL.thy "(A --> B & C) = ((A --> B) & (A --> C))";
    5.17 -  by (fast_tac HOL_cs 1);
    5.18 +  by (Fast_tac 1);
    5.19  qed "fork_lemma";
    5.20  
    5.21  goal HOL.thy "((A --> B) & (C --> B)) = ((A | C) --> B)";
    5.22 -  by (fast_tac HOL_cs 1);
    5.23 +  by (Fast_tac 1);
    5.24  qed "imp_or_lem";
    5.25  
    5.26  goal HOL.thy "(X = (~ Y)) = ((~X) = Y)";
    5.27 -  by (fast_tac HOL_cs 1);
    5.28 +  by (Fast_tac 1);
    5.29  qed "neg_flip";
    5.30  
    5.31  goal HOL.thy "P --> Q(M) --> Q(if P then M else N)";
    5.32    by (rtac impI 1); 
    5.33    by (rtac impI 1);
    5.34    by (rtac (expand_if RS iffD2) 1);
    5.35 -  by (fast_tac HOL_cs 1);
    5.36 +  by (Fast_tac 1);
    5.37  qed "imp_true_decompose";
    5.38  
    5.39  goal HOL.thy "(~P) --> Q(N) --> Q(if P then M else N)";
    5.40    by (rtac impI 1); 
    5.41    by (rtac impI 1);
    5.42    by (rtac (expand_if RS iffD2) 1);
    5.43 -  by (fast_tac HOL_cs 1);
    5.44 +  by (Fast_tac 1);
    5.45  qed "imp_false_decompose";
    5.46  
    5.47  
    5.48  (* Sets *)
    5.49  val set_lemmas =
    5.50 -   map (fn s => prove_goal Set.thy s (fn _ => [fast_tac set_cs 1]))
    5.51 +   map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1]))
    5.52          ["f(x) : (UN x. {f(x)})",
    5.53           "f x y : (UN x y. {f x y})",
    5.54           "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})",
    5.55 @@ -75,7 +75,7 @@
    5.56    by (nat_ind_tac "x" 1);
    5.57    by (Simp_tac 1);
    5.58    by (Asm_simp_tac 1);
    5.59 -  by (fast_tac HOL_cs 1);
    5.60 +  by (Fast_tac 1);
    5.61  qed "nonzero_is_succ";
    5.62  
    5.63  goal Arith.thy "(m::nat) < n --> m + p < n + p";
    5.64 @@ -96,7 +96,7 @@
    5.65    by (Asm_simp_tac 1);
    5.66    by (rtac impI 1);
    5.67    by (dtac Suc_leD 1);
    5.68 -  by (fast_tac HOL_cs 1);
    5.69 +  by (Fast_tac 1);
    5.70  qed "left_add_leq";
    5.71  
    5.72  goal Arith.thy "(A::nat) < B --> C < D --> A + C < B + D";
    5.73 @@ -115,7 +115,7 @@
    5.74    by (rtac impI 1);
    5.75    by (rtac impI 1);
    5.76    by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
    5.77 -  by (safe_tac HOL_cs);
    5.78 +  by (safe_tac (!claset));
    5.79    by (rtac (less_add_cong RS mp RS mp) 1);
    5.80    by (assume_tac 1);
    5.81    by (assume_tac 1);
    5.82 @@ -143,21 +143,21 @@
    5.83    by (Simp_tac 1);
    5.84    by (rtac iffI 1);
    5.85    by (Asm_full_simp_tac 1);
    5.86 -  by (fast_tac HOL_cs 1);
    5.87 +  by (Fast_tac 1);
    5.88  qed "suc_not_zero";
    5.89  
    5.90  goal Arith.thy "Suc(x) <= y --> (? z. y = Suc(z))";
    5.91    by (rtac impI 1);
    5.92    by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
    5.93 -  by (safe_tac HOL_cs);
    5.94 -  by (fast_tac HOL_cs 2);
    5.95 +  by (safe_tac (!claset));
    5.96 +  by (Fast_tac 2);
    5.97    by (asm_simp_tac (!simpset addsimps [suc_not_zero]) 1);
    5.98  qed "suc_leq_suc";
    5.99  
   5.100  goal Arith.thy "~0<n --> n = 0";
   5.101    by (nat_ind_tac "n" 1);
   5.102    by (Asm_simp_tac 1);
   5.103 -  by (safe_tac HOL_cs);
   5.104 +  by (safe_tac (!claset));
   5.105    by (Asm_full_simp_tac 1);
   5.106    by (Asm_full_simp_tac 1);
   5.107  qed "zero_eq";
   5.108 @@ -165,7 +165,7 @@
   5.109  goal Arith.thy "x < Suc(y) --> x<=y";
   5.110    by (nat_ind_tac "n" 1);
   5.111    by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   5.112 -  by (safe_tac HOL_cs);
   5.113 +  by (safe_tac (!claset));
   5.114    by (etac less_imp_le 1);
   5.115  qed "less_suc_imp_leq";
   5.116  
     6.1 --- a/src/HOL/IOA/NTP/Multiset.ML	Mon Jul 29 18:31:39 1996 +0200
     6.2 +++ b/src/HOL/IOA/NTP/Multiset.ML	Tue Jul 30 17:33:26 1996 +0200
     6.3 @@ -34,7 +34,7 @@
     6.4                           addsimps [Multiset.delm_nonempty_def,
     6.5                                     Multiset.countm_nonempty_def]
     6.6                           setloop (split_tac [expand_if])) 1);
     6.7 -  by (safe_tac HOL_cs);
     6.8 +  by (safe_tac (!claset));
     6.9    by (Asm_full_simp_tac 1);
    6.10  qed "count_delm_simp";
    6.11  
     7.1 --- a/src/HOL/IOA/meta_theory/IOA.ML	Mon Jul 29 18:31:39 1996 +0200
     7.2 +++ b/src/HOL/IOA/meta_theory/IOA.ML	Tue Jul 30 17:33:26 1996 +0200
     7.3 @@ -41,7 +41,7 @@
     7.4  \   (s(n)=Some(a) & a : externals(asig_of(A)))";
     7.5    by (Option.option.induct_tac "s(n)" 1);
     7.6    by (ALLGOALS (simp_tac (!simpset setloop (split_tac [expand_if]))));
     7.7 -  by (fast_tac HOL_cs 1);
     7.8 +  by (Fast_tac 1);
     7.9  qed "mk_trace_thm";
    7.10  
    7.11  goalw IOA.thy [reachable_def] "!!A. s:starts_of(A) ==> reachable A s";
    7.12 @@ -53,7 +53,7 @@
    7.13  goalw IOA.thy (reachable_def::exec_rws)
    7.14  "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t";
    7.15    by(Asm_full_simp_tac 1);
    7.16 -  by(safe_tac set_cs);
    7.17 +  by(safe_tac (!claset));
    7.18    by(res_inst_tac [("x","(%i.if i<n then fst ex i                    \
    7.19  \                            else (if i=n then Some a else None),    \
    7.20  \                         %i.if i<Suc n then snd ex i else t)")] bexI 1);
    7.21 @@ -66,7 +66,7 @@
    7.22    by(asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
    7.23    be disjE 1;
    7.24    by(Asm_simp_tac 1);
    7.25 -  by(fast_tac HOL_cs 1);
    7.26 +  by(Fast_tac 1);
    7.27    by(forward_tac [less_not_sym] 1);
    7.28    by(asm_simp_tac (!simpset addsimps [less_not_refl2,less_Suc_eq]) 1);
    7.29  qed "reachable_n";
    7.30 @@ -76,16 +76,16 @@
    7.31  \     !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \
    7.32  \  ==> invariant A P";
    7.33    by (rewrite_goals_tac(reachable_def::Let_def::exec_rws));
    7.34 -  by (safe_tac set_cs);
    7.35 +  by (safe_tac (!claset));
    7.36    by (res_inst_tac [("Q","reachable A (snd ex n)")] conjunct1 1);
    7.37    by (nat_ind_tac "n" 1);
    7.38 -  by (fast_tac (set_cs addIs [p1,reachable_0]) 1);
    7.39 +  by (fast_tac (!claset addIs [p1,reachable_0]) 1);
    7.40    by (eres_inst_tac[("x","n1")]allE 1);
    7.41    by (eres_inst_tac[("P","%x.!a.?Q x a"), ("opt","fst ex n1")] optE 1);
    7.42    by (Asm_simp_tac 1);
    7.43 -  by (safe_tac HOL_cs);
    7.44 +  by (safe_tac (!claset));
    7.45    by (etac (p2 RS mp) 1);
    7.46 -  by (ALLGOALS(fast_tac(set_cs addDs [hd Option.option.inject RS iffD1,
    7.47 +  by (ALLGOALS(fast_tac(!claset addDs [hd Option.option.inject RS iffD1,
    7.48                                        reachable_n])));
    7.49  qed "invariantI";
    7.50  
    7.51 @@ -93,7 +93,7 @@
    7.52   "[| !!s. s : starts_of(A) ==> P(s); \
    7.53  \   !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
    7.54  \ |] ==> invariant A P";
    7.55 -  by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1);
    7.56 +  by (fast_tac (!claset addSIs [invariantI] addSDs [p1,p2]) 1);
    7.57  qed "invariantI1";
    7.58  
    7.59  val [p1,p2] = goalw IOA.thy [invariant_def]
    7.60 @@ -116,7 +116,7 @@
    7.61  (* Every state in an execution is reachable *)
    7.62  goalw IOA.thy [reachable_def] 
    7.63  "!!A. ex:executions(A) ==> !n. reachable A (snd ex n)";
    7.64 -  by (fast_tac set_cs 1);
    7.65 +  by (Fast_tac 1);
    7.66  qed "states_of_exec_reachable";
    7.67  
    7.68  
    7.69 @@ -155,19 +155,19 @@
    7.70  \  (externals(asig_of(A1)) Un externals(asig_of(A2)))";
    7.71  by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1);
    7.72  by (rtac set_ext 1); 
    7.73 -by (fast_tac set_cs 1);
    7.74 +by (Fast_tac 1);
    7.75  qed"externals_of_par"; 
    7.76  
    7.77  goalw IOA.thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
    7.78   "!! a. [| compat_ioas A1 A2; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))";
    7.79  by (Asm_full_simp_tac 1);
    7.80 -by (best_tac (set_cs addEs [equalityCE]) 1);
    7.81 +by (best_tac (!claset addEs [equalityCE]) 1);
    7.82  qed"ext1_is_not_int2";
    7.83  
    7.84  goalw IOA.thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
    7.85   "!! a. [| compat_ioas A2 A1 ; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))";
    7.86  by (Asm_full_simp_tac 1);
    7.87 -by (best_tac (set_cs addEs [equalityCE]) 1);
    7.88 +by (best_tac (!claset addEs [equalityCE]) 1);
    7.89  qed"ext2_is_not_int1";
    7.90  
    7.91  val ext1_ext2_is_not_act2 = ext1_is_not_int2 RS int_and_ext_is_act;
     8.1 --- a/src/HOL/IOA/meta_theory/Option.ML	Mon Jul 29 18:31:39 1996 +0200
     8.2 +++ b/src/HOL/IOA/meta_theory/Option.ML	Tue Jul 30 17:33:26 1996 +0200
     8.3 @@ -11,7 +11,7 @@
     8.4  val [prem] = goal Option.thy "P(opt) ==> P(None) | (? x. P(Some(x)))";
     8.5   br (prem RS rev_mp) 1;
     8.6   by (Option.option.induct_tac "opt" 1);
     8.7 - by (ALLGOALS(fast_tac HOL_cs));
     8.8 + by (ALLGOALS(Fast_tac));
     8.9  val optE = store_thm("optE", standard(result() RS disjE));
    8.10  
    8.11  goal Option.thy "x=None | (? y.x=Some(y))"; 
     9.1 --- a/src/HOL/IOA/meta_theory/Solve.ML	Mon Jul 29 18:31:39 1996 +0200
     9.2 +++ b/src/HOL/IOA/meta_theory/Solve.ML	Tue Jul 30 17:33:26 1996 +0200
     9.3 @@ -15,7 +15,7 @@
     9.4  \          is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
     9.5  
     9.6    by (simp_tac(!simpset addsimps [has_trace_def])1);
     9.7 -  by (safe_tac set_cs);
     9.8 +  by (safe_tac (!claset));
     9.9  
    9.10    (* choose same trace, therefore same NF *)
    9.11    by (res_inst_tac[("x","mk_trace  C (fst ex)")] exI 1);
    9.12 @@ -32,7 +32,7 @@
    9.13  
    9.14    (* Now show that it's an execution *)
    9.15    by (asm_full_simp_tac(!simpset addsimps [executions_def]) 1);
    9.16 -  by (safe_tac set_cs);
    9.17 +  by (safe_tac (!claset));
    9.18  
    9.19    (* Start states map to start states *)
    9.20    by (dtac bspec 1);
    9.21 @@ -40,7 +40,7 @@
    9.22  
    9.23    (* Show that it's an execution fragment *)
    9.24    by (asm_full_simp_tac (!simpset addsimps [is_execution_fragment_def])1);
    9.25 -  by (safe_tac HOL_cs);
    9.26 +  by (safe_tac (!claset));
    9.27  
    9.28    by (eres_inst_tac [("x","snd ex n")] allE 1);
    9.29    by (eres_inst_tac [("x","snd ex (Suc n)")] allE 1);
    9.30 @@ -51,7 +51,7 @@
    9.31  (* Lemmata *)
    9.32  
    9.33  val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    9.34 -  by(fast_tac (HOL_cs addDs prems) 1);
    9.35 +  by(fast_tac (!claset addDs prems) 1);
    9.36  val imp_conj_lemma = result();
    9.37  
    9.38  
    9.39 @@ -61,7 +61,7 @@
    9.40  \  a:externals(asig_of(A1)) & a~:externals(asig_of(A2)) |  \
    9.41  \  a~:externals(asig_of(A1)) & a:externals(asig_of(A2)))";
    9.42  by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def]) 1);
    9.43 - by (fast_tac set_cs 1);
    9.44 + by (Fast_tac 1);
    9.45  val externals_of_par_extra = result(); 
    9.46  
    9.47  goal Solve.thy "!!s.[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
    9.48 @@ -73,7 +73,7 @@
    9.49  \    %i.fst (snd ex i))")]  bexI 1);
    9.50  (* fst(s) is in projected execution *)
    9.51   by (Simp_tac 1);
    9.52 - by (fast_tac HOL_cs 1);
    9.53 + by (Fast_tac 1);
    9.54  (* projected execution is indeed an execution *)
    9.55  by (asm_full_simp_tac (!simpset addsimps [executions_def,is_execution_fragment_def,
    9.56      par_def, starts_of_def,trans_of_def]) 1);
    9.57 @@ -108,7 +108,7 @@
    9.58  \    %i.snd (snd ex i))")]  bexI 1);
    9.59  (* fst(s) is in projected execution *)
    9.60   by (Simp_tac 1);
    9.61 - by (fast_tac HOL_cs 1);
    9.62 + by (Fast_tac 1);
    9.63  (* projected execution is indeed an execution *)
    9.64   by (asm_full_simp_tac (!simpset addsimps [executions_def,is_execution_fragment_def,
    9.65      par_def, starts_of_def,trans_of_def]) 1);
    9.66 @@ -138,7 +138,7 @@
    9.67   by (rtac conjI 1);
    9.68  (* start_states *)
    9.69   by (asm_full_simp_tac (!simpset addsimps [par_def, starts_of_def]) 1);
    9.70 - by (fast_tac set_cs 1);
    9.71 + by (Fast_tac 1);
    9.72  (* transitions *)
    9.73  by (REPEAT (rtac allI 1));
    9.74  by (rtac imp_conj_lemma 1);
    9.75 @@ -165,7 +165,7 @@
    9.76  by (subgoal_tac "a~:externals(asig_of(A1)) & a~:externals(asig_of(A2))" 1);
    9.77  (* delete auxiliary subgoal *)
    9.78  by (Asm_full_simp_tac 2);
    9.79 -by (fast_tac HOL_cs 2);
    9.80 +by (Fast_tac 2);
    9.81  by (simp_tac (!simpset addsimps [conj_disj_distribR] addcongs [conj_cong]
    9.82                   setloop (split_tac [expand_if])) 1);
    9.83  by(REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
    9.84 @@ -202,19 +202,19 @@
    9.85  by (dtac sym 1);
    9.86  by (dtac sym 1);
    9.87  by (Asm_full_simp_tac 1);
    9.88 -by (safe_tac HOL_cs);
    9.89 +by (safe_tac (!claset));
    9.90  qed"reachable_rename_ioa";
    9.91  
    9.92  
    9.93  (* HOL Lemmata - must already exist ! *)
    9.94  goal HOL.thy  "(~(A|B)) =(~A&~B)";
    9.95 - by (fast_tac HOL_cs 1);
    9.96 + by (Fast_tac 1);
    9.97  val disj_demorgan = result();
    9.98  goal HOL.thy  "(~(A&B)) =(~A|~B)";
    9.99 - by (fast_tac HOL_cs 1);
   9.100 + by (Fast_tac 1);
   9.101  val conj_demorgan = result();
   9.102  goal HOL.thy  "(~(? x.P x)) =(! x. (~ (P x)))";
   9.103 - by (fast_tac HOL_cs 1);
   9.104 + by (Fast_tac 1);
   9.105  val neg_ex = result();
   9.106  
   9.107  
   9.108 @@ -227,7 +227,7 @@
   9.109  by (rtac imp_conj_lemma 1);
   9.110  by (simp_tac (!simpset addsimps [rename_def]) 1);
   9.111  by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1);
   9.112 -by (safe_tac set_cs);
   9.113 +by (safe_tac (!claset));
   9.114  by (rtac (expand_if RS ssubst) 1);
   9.115   by (rtac conjI 1);
   9.116   by (rtac impI 1);
    10.1 --- a/src/HOL/Integ/Bin.ML	Mon Jul 29 18:31:39 1996 +0200
    10.2 +++ b/src/HOL/Integ/Bin.ML	Tue Jul 30 17:33:26 1996 +0200
    10.3 @@ -54,7 +54,7 @@
    10.4  
    10.5  (* SHOULD THIS THEOREM BE ADDED TO HOL_SS ? *)
    10.6  val my = prove_goal HOL.thy "(False = (~P)) = P"
    10.7 -	(fn prem => [(fast_tac HOL_cs 1)]);
    10.8 +	(fn prem => [(Fast_tac 1)]);
    10.9  
   10.10  qed_goal "bin_add_Bcons_Bcons0" Bin.thy "bin_add (Bcons v False) (Bcons w y) = norm_Bcons (bin_add v w) y"
   10.11  	(fn prem => [(simp_tac (!simpset addsimps [my]) 1)]);
   10.12 @@ -141,7 +141,7 @@
   10.13  
   10.14  goal Bin.thy "integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
   10.15  by (cut_facts_tac [integ_of_bin_add_lemma] 1);
   10.16 -by (fast_tac HOL_cs 1);
   10.17 +by (Fast_tac 1);
   10.18  qed "integ_of_bin_add";
   10.19  
   10.20  val bin_mult_simps = [integ_of_bin_minus, integ_of_bin_add,integ_of_bin_norm_Bcons];
    11.1 --- a/src/HOL/Integ/Equiv.ML	Mon Jul 29 18:31:39 1996 +0200
    11.2 +++ b/src/HOL/Integ/Equiv.ML	Tue Jul 30 17:33:26 1996 +0200
    11.3 @@ -10,18 +10,20 @@
    11.4  
    11.5  open Equiv;
    11.6  
    11.7 +Delrules [equalityI];
    11.8 +
    11.9  (*** Suppes, Theorem 70: r is an equiv relation iff converse(r) O r = r ***)
   11.10  
   11.11  (** first half: equiv A r ==> converse(r) O r = r **)
   11.12  
   11.13  goalw Equiv.thy [trans_def,sym_def,converse_def]
   11.14      "!!r. [| sym(r); trans(r) |] ==> converse(r) O r <= r";
   11.15 -by (fast_tac (comp_cs addSEs [converseD]) 1);
   11.16 +by (fast_tac (!claset addSEs [converseD]) 1);
   11.17  qed "sym_trans_comp_subset";
   11.18  
   11.19  goalw Equiv.thy [refl_def]
   11.20      "!!A r. refl A r ==> r <= converse(r) O r";
   11.21 -by (fast_tac (rel_cs addIs [compI]) 1);
   11.22 +by (fast_tac (!claset addIs [compI]) 1);
   11.23  qed "refl_comp_subset";
   11.24  
   11.25  goalw Equiv.thy [equiv_def]
   11.26 @@ -36,9 +38,9 @@
   11.27      "!!A r. [| converse(r) O r = r;  Domain(r) = A |] ==> equiv A r";
   11.28  by (etac equalityE 1);
   11.29  by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1);
   11.30 -by (safe_tac set_cs);
   11.31 -by (fast_tac (set_cs addSIs [converseI] addIs [compI]) 3);
   11.32 -by (ALLGOALS (fast_tac (rel_cs addIs [compI] addSEs [compE])));
   11.33 +by (safe_tac (!claset));
   11.34 +by (fast_tac (!claset addSIs [converseI] addIs [compI]) 3);
   11.35 +by (ALLGOALS (fast_tac (!claset addIs [compI] addSEs [compE])));
   11.36  qed "comp_equivI";
   11.37  
   11.38  (** Equivalence classes **)
   11.39 @@ -46,28 +48,28 @@
   11.40  (*Lemma for the next result*)
   11.41  goalw Equiv.thy [equiv_def,trans_def,sym_def]
   11.42      "!!A r. [| equiv A r;  (a,b): r |] ==> r^^{a} <= r^^{b}";
   11.43 -by (safe_tac rel_cs);
   11.44 +by (safe_tac (!claset));
   11.45  by (rtac ImageI 1);
   11.46 -by (fast_tac rel_cs 2);
   11.47 -by (fast_tac rel_cs 1);
   11.48 +by (Fast_tac 2);
   11.49 +by (Fast_tac 1);
   11.50  qed "equiv_class_subset";
   11.51  
   11.52  goal Equiv.thy "!!A r. [| equiv A r;  (a,b): r |] ==> r^^{a} = r^^{b}";
   11.53  by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1));
   11.54  by (rewrite_goals_tac [equiv_def,sym_def]);
   11.55 -by (fast_tac rel_cs 1);
   11.56 +by (Fast_tac 1);
   11.57  qed "equiv_class_eq";
   11.58  
   11.59  val prems = goalw Equiv.thy [equiv_def,refl_def]
   11.60      "[| equiv A r;  a: A |] ==> a: r^^{a}";
   11.61  by (cut_facts_tac prems 1);
   11.62 -by (fast_tac rel_cs 1);
   11.63 +by (Fast_tac 1);
   11.64  qed "equiv_class_self";
   11.65  
   11.66  (*Lemma for the next result*)
   11.67  goalw Equiv.thy [equiv_def,refl_def]
   11.68      "!!A r. [| equiv A r;  r^^{b} <= r^^{a};  b: A |] ==> (a,b): r";
   11.69 -by (fast_tac rel_cs 1);
   11.70 +by (Fast_tac 1);
   11.71  qed "subset_equiv_class";
   11.72  
   11.73  val prems = goal Equiv.thy
   11.74 @@ -78,7 +80,7 @@
   11.75  (*thus r^^{a} = r^^{b} as well*)
   11.76  goalw Equiv.thy [equiv_def,trans_def,sym_def]
   11.77      "!!A r. [| equiv A r;  x: (r^^{a} Int r^^{b}) |] ==> (a,b): r";
   11.78 -by (fast_tac rel_cs 1);
   11.79 +by (Fast_tac 1);
   11.80  qed "equiv_class_nondisjoint";
   11.81  
   11.82  val [major] = goalw Equiv.thy [equiv_def,refl_def]
   11.83 @@ -88,7 +90,7 @@
   11.84  
   11.85  goal Equiv.thy
   11.86      "!!A r. equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
   11.87 -by (safe_tac rel_cs);
   11.88 +by (safe_tac (!claset));
   11.89  by ((rtac equiv_class_eq 1) THEN (assume_tac 1) THEN (assume_tac 1));
   11.90  by ((rtac eq_equiv_class 3) THEN 
   11.91      (assume_tac 4) THEN (assume_tac 4) THEN (assume_tac 3));
   11.92 @@ -100,7 +102,7 @@
   11.93  
   11.94  goal Equiv.thy
   11.95      "!!A r. [| equiv A r;  x: A;  y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
   11.96 -by (safe_tac rel_cs);
   11.97 +by (safe_tac (!claset));
   11.98  by ((rtac eq_equiv_class 1) THEN 
   11.99      (assume_tac 1) THEN (assume_tac 1) THEN (assume_tac 1));
  11.100  by ((rtac equiv_class_eq 1) THEN 
  11.101 @@ -123,7 +125,7 @@
  11.102  by (resolve_tac [major RS UN_E] 1);
  11.103  by (rtac minor 1);
  11.104  by (assume_tac 2);
  11.105 -by (fast_tac rel_cs 1);
  11.106 +by (Fast_tac 1);
  11.107  qed "quotientE";
  11.108  
  11.109  (** Not needed by Theory Integ --> bypassed **)
  11.110 @@ -136,10 +138,10 @@
  11.111  (** Not needed by Theory Integ --> bypassed **)
  11.112  (*goalw Equiv.thy [quotient_def]
  11.113      "!!A r. [| equiv A r;  X: A/r;  Y: A/r |] ==> X=Y | (X Int Y <= 0)";
  11.114 -by (safe_tac (ZF_cs addSIs [equiv_class_eq]));
  11.115 +by (safe_tac (!claset addSIs [equiv_class_eq]));
  11.116  by (assume_tac 1);
  11.117  by (rewrite_goals_tac [equiv_def,trans_def,sym_def]);
  11.118 -by (fast_tac ZF_cs 1);
  11.119 +by (Fast_tac 1);
  11.120  qed "quotient_disj";
  11.121  **)
  11.122  
  11.123 @@ -147,7 +149,7 @@
  11.124  
  11.125  (* theorem needed to prove UN_equiv_class *)
  11.126  goal Set.thy "!!A. [| a:A; ! y:A. b(y)=b(a) |] ==> (UN y:A. b(y))=b(a)";
  11.127 -by (fast_tac (!claset addSEs [equalityE]) 1);
  11.128 +by (fast_tac (!claset addSEs [equalityE] addSIs [equalityI]) 1);
  11.129  qed "UN_singleton_lemma";
  11.130  val UN_singleton = ballI RSN (2,UN_singleton_lemma);
  11.131  
  11.132 @@ -165,7 +167,7 @@
  11.133  by (assume_tac 1);
  11.134  by (assume_tac 1);
  11.135  by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]);
  11.136 -by (fast_tac rel_cs 1);
  11.137 +by (Fast_tac 1);
  11.138  qed "UN_equiv_class";
  11.139  
  11.140  (*Resolve th against the "local" premises*)
  11.141 @@ -177,7 +179,7 @@
  11.142  \       !!x.  x : A ==> b(x) : B |]     \
  11.143  \    ==> (UN x:X. b(x)) : B";
  11.144  by (cut_facts_tac prems 1);
  11.145 -by (safe_tac rel_cs);
  11.146 +by (safe_tac (!claset));
  11.147  by (rtac (localize UN_equiv_class RS ssubst) 1);
  11.148  by (REPEAT (ares_tac prems 1));
  11.149  qed "UN_equiv_class_type";
  11.150 @@ -191,7 +193,7 @@
  11.151  \       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |]         \
  11.152  \    ==> X=Y";
  11.153  by (cut_facts_tac prems 1);
  11.154 -by (safe_tac rel_cs);
  11.155 +by (safe_tac ((!claset) delrules [equalityI]));
  11.156  by (rtac (equivA RS equiv_class_eq) 1);
  11.157  by (REPEAT (ares_tac prems 1));
  11.158  by (etac box_equals 1);
  11.159 @@ -204,20 +206,20 @@
  11.160  
  11.161  goalw Equiv.thy [congruent_def,congruent2_def,equiv_def,refl_def]
  11.162      "!!A r. [| equiv A r;  congruent2 r b;  a: A |] ==> congruent r (b a)";
  11.163 -by (fast_tac rel_cs 1);
  11.164 +by (Fast_tac 1);
  11.165  qed "congruent2_implies_congruent";
  11.166  
  11.167  val equivA::prems = goalw Equiv.thy [congruent_def]
  11.168      "[| equiv A r;  congruent2 r b;  a: A |] ==> \
  11.169  \    congruent r (%x1. UN x2:r^^{a}. b x1 x2)";
  11.170  by (cut_facts_tac (equivA::prems) 1);
  11.171 -by (safe_tac rel_cs);
  11.172 +by (safe_tac (!claset));
  11.173  by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
  11.174  by (assume_tac 1);
  11.175  by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class,
  11.176                                       congruent2_implies_congruent]) 1);
  11.177  by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
  11.178 -by (fast_tac rel_cs 1);
  11.179 +by (Fast_tac 1);
  11.180  qed "congruent2_implies_congruent_UN";
  11.181  
  11.182  val prems as equivA::_ = goal Equiv.thy
  11.183 @@ -236,7 +238,7 @@
  11.184  \       !!x1 x2.  [| x1: A; x2: A |] ==> b x1 x2 : B |]    \
  11.185  \    ==> (UN x1:X1. UN x2:X2. b x1 x2) : B";
  11.186  by (cut_facts_tac prems 1);
  11.187 -by (safe_tac rel_cs);
  11.188 +by (safe_tac (!claset));
  11.189  by (REPEAT (ares_tac (prems@[UN_equiv_class_type,
  11.190                               congruent2_implies_congruent_UN,
  11.191                               congruent2_implies_congruent, quotientI]) 1));
  11.192 @@ -251,7 +253,7 @@
  11.193  \       !! y z w. [| w: A;  (y,z) : r |] ==> b w y = b w z       \
  11.194  \    |] ==> congruent2 r b";
  11.195  by (cut_facts_tac prems 1);
  11.196 -by (safe_tac rel_cs);
  11.197 +by (safe_tac (!claset));
  11.198  by (rtac trans 1);
  11.199  by (REPEAT (ares_tac prems 1
  11.200       ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1));
    12.1 --- a/src/HOL/Integ/Integ.ML	Mon Jul 29 18:31:39 1996 +0200
    12.2 +++ b/src/HOL/Integ/Integ.ML	Tue Jul 30 17:33:26 1996 +0200
    12.3 @@ -16,6 +16,8 @@
    12.4  
    12.5  open Integ;
    12.6  
    12.7 +Delrules [equalityI];
    12.8 +
    12.9  
   12.10  (*** Proving that intrel is an equivalence relation ***)
   12.11  
   12.12 @@ -35,14 +37,14 @@
   12.13  val prems = goalw Integ.thy [intrel_def]
   12.14      "[| x1+y2 = x2+y1|] ==> \
   12.15  \    ((x1,y1),(x2,y2)): intrel";
   12.16 -by (fast_tac (rel_cs addIs prems) 1);
   12.17 +by (fast_tac (!claset addIs prems) 1);
   12.18  qed "intrelI";
   12.19  
   12.20  (*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
   12.21  goalw Integ.thy [intrel_def]
   12.22    "p: intrel --> (EX x1 y1 x2 y2. \
   12.23  \                  p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1)";
   12.24 -by (fast_tac rel_cs 1);
   12.25 +by (Fast_tac 1);
   12.26  qed "intrelE_lemma";
   12.27  
   12.28  val [major,minor] = goal Integ.thy
   12.29 @@ -53,10 +55,11 @@
   12.30  by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
   12.31  qed "intrelE";
   12.32  
   12.33 -val intrel_cs = rel_cs addSIs [intrelI] addSEs [intrelE];
   12.34 +AddSIs [intrelI];
   12.35 +AddSEs [intrelE];
   12.36  
   12.37  goal Integ.thy "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)";
   12.38 -by (fast_tac intrel_cs 1);
   12.39 +by (Fast_tac 1);
   12.40  qed "intrel_iff";
   12.41  
   12.42  goal Integ.thy "(x,x): intrel";
   12.43 @@ -65,7 +68,7 @@
   12.44  
   12.45  goalw Integ.thy [equiv_def, refl_def, sym_def, trans_def]
   12.46      "equiv {x::(nat*nat).True} intrel";
   12.47 -by (fast_tac (intrel_cs addSIs [intrel_refl] 
   12.48 +by (fast_tac (!claset addSIs [intrel_refl] 
   12.49                          addSEs [sym, integ_trans_lemma]) 1);
   12.50  qed "equiv_intrel";
   12.51  
   12.52 @@ -75,7 +78,7 @@
   12.53      (equiv_intrel RS eq_equiv_class_iff));
   12.54  
   12.55  goalw Integ.thy  [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ";
   12.56 -by (fast_tac set_cs 1);
   12.57 +by (Fast_tac 1);
   12.58  qed "intrel_in_integ";
   12.59  
   12.60  goal Integ.thy "inj_onto Abs_Integ Integ";
   12.61 @@ -103,8 +106,8 @@
   12.62  by (REPEAT (rtac intrel_in_integ 1));
   12.63  by (dtac eq_equiv_class 1);
   12.64  by (rtac equiv_intrel 1);
   12.65 -by (fast_tac set_cs 1);
   12.66 -by (safe_tac intrel_cs);
   12.67 +by (Fast_tac 1);
   12.68 +by (safe_tac (!claset));
   12.69  by (Asm_full_simp_tac 1);
   12.70  qed "inj_znat";
   12.71  
   12.72 @@ -113,7 +116,7 @@
   12.73  
   12.74  goalw Integ.thy [congruent_def]
   12.75    "congruent intrel (%p. split (%x y. intrel^^{(y,x)}) p)";
   12.76 -by (safe_tac intrel_cs);
   12.77 +by (safe_tac (!claset));
   12.78  by (asm_simp_tac (!simpset addsimps add_ac) 1);
   12.79  qed "zminus_congruent";
   12.80  
   12.81 @@ -168,12 +171,12 @@
   12.82  goalw Integ.thy [znegative_def, znat_def]
   12.83      "~ znegative($# n)";
   12.84  by (Simp_tac 1);
   12.85 -by (safe_tac intrel_cs);
   12.86 +by (safe_tac (!claset));
   12.87  by (rtac ccontr 1);
   12.88  by (etac notE 1);
   12.89  by (Asm_full_simp_tac 1);
   12.90  by (dtac not_znegative_znat_lemma 1);
   12.91 -by (fast_tac (HOL_cs addDs [leD]) 1);
   12.92 +by (fast_tac (!claset addDs [leD]) 1);
   12.93  qed "not_znegative_znat";
   12.94  
   12.95  goalw Integ.thy [znegative_def, znat_def] "znegative($~ $# Suc(n))";
   12.96 @@ -200,7 +203,7 @@
   12.97  
   12.98  goalw Integ.thy [congruent_def]
   12.99      "congruent intrel (split (%x y. intrel^^{((y-x) + (x-(y::nat)),0)}))";
  12.100 -by (safe_tac intrel_cs);
  12.101 +by (safe_tac (!claset));
  12.102  by (Asm_simp_tac 1);
  12.103  by (etac rev_mp 1);
  12.104  by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1);
  12.105 @@ -245,7 +248,7 @@
  12.106      "congruent2 intrel (%p1 p2.                  \
  12.107  \         split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)";
  12.108  (*Proof via congruent2_commuteI seems longer*)
  12.109 -by (safe_tac intrel_cs);
  12.110 +by (safe_tac (!claset));
  12.111  by (asm_simp_tac (!simpset addsimps [add_assoc]) 1);
  12.112  (*The rest should be trivial, but rearranging terms is hard*)
  12.113  by (res_inst_tac [("x1","x1a")] (add_left_commute RS ssubst) 1);
  12.114 @@ -332,7 +335,7 @@
  12.115  \               split (%x1 y1. split (%x2 y2.   \
  12.116  \                   intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
  12.117  by (rtac (equiv_intrel RS congruent2_commuteI) 1);
  12.118 -by (safe_tac intrel_cs);
  12.119 +by (safe_tac (!claset));
  12.120  by (rewtac split_def);
  12.121  by (simp_tac (!simpset addsimps add_ac@mult_ac) 1);
  12.122  by (asm_simp_tac (!simpset delsimps [equiv_intrel_iff]
  12.123 @@ -466,31 +469,31 @@
  12.124  qed "zsuc_zpred";
  12.125  
  12.126  goal Integ.thy "(zpred(z)=w) = (z=zsuc(w))";
  12.127 -by (safe_tac HOL_cs);
  12.128 +by (safe_tac (!claset));
  12.129  by (rtac (zsuc_zpred RS sym) 1);
  12.130  by (rtac zpred_zsuc 1);
  12.131  qed "zpred_to_zsuc";
  12.132  
  12.133  goal Integ.thy "(zsuc(z)=w)=(z=zpred(w))";
  12.134 -by (safe_tac HOL_cs);
  12.135 +by (safe_tac (!claset));
  12.136  by (rtac (zpred_zsuc RS sym) 1);
  12.137  by (rtac zsuc_zpred 1);
  12.138  qed "zsuc_to_zpred";
  12.139  
  12.140  goal Integ.thy "($~ z = w) = (z = $~ w)";
  12.141 -by (safe_tac HOL_cs);
  12.142 +by (safe_tac (!claset));
  12.143  by (rtac (zminus_zminus RS sym) 1);
  12.144  by (rtac zminus_zminus 1);
  12.145  qed "zminus_exchange";
  12.146  
  12.147  goal Integ.thy"(zsuc(z)=zsuc(w)) = (z=w)";
  12.148 -by (safe_tac intrel_cs);
  12.149 +by (safe_tac (!claset));
  12.150  by (dres_inst_tac [("f","zpred")] arg_cong 1);
  12.151  by (asm_full_simp_tac (!simpset addsimps [zpred_zsuc]) 1);
  12.152  qed "bijective_zsuc";
  12.153  
  12.154  goal Integ.thy"(zpred(z)=zpred(w)) = (z=w)";
  12.155 -by (safe_tac intrel_cs);
  12.156 +by (safe_tac (!claset));
  12.157  by (dres_inst_tac [("f","zsuc")] arg_cong 1);
  12.158  by (asm_full_simp_tac (!simpset addsimps [zsuc_zpred]) 1);
  12.159  qed "bijective_zpred";
  12.160 @@ -549,7 +552,7 @@
  12.161  val zsuc_n_not_n = n_not_zsuc_n RS not_sym;
  12.162  
  12.163  goal Integ.thy "w ~= zpred(w)";
  12.164 -by (safe_tac HOL_cs);
  12.165 +by (safe_tac (!claset));
  12.166  by (dres_inst_tac [("x","w"),("f","zsuc")] arg_cong 1);
  12.167  by (asm_full_simp_tac (!simpset addsimps [zsuc_zpred,zsuc_n_not_n]) 1);
  12.168  qed "n_not_zpred_n";
  12.169 @@ -563,9 +566,9 @@
  12.170      "!!w. w<z ==> ? n. z = w + $#(Suc(n))";
  12.171  by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
  12.172  by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
  12.173 -by (safe_tac intrel_cs);
  12.174 +by (safe_tac (!claset));
  12.175  by (asm_full_simp_tac (!simpset addsimps [zadd, zminus]) 1);
  12.176 -by (safe_tac (intrel_cs addSDs [less_eq_Suc_add]));
  12.177 +by (safe_tac (!claset addSDs [less_eq_Suc_add]));
  12.178  by (res_inst_tac [("x","k")] exI 1);
  12.179  by (asm_full_simp_tac (!simpset delsimps [add_Suc, add_Suc_right]
  12.180                                  addsimps ([add_Suc RS sym] @ add_ac)) 1);
  12.181 @@ -578,7 +581,7 @@
  12.182  goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] 
  12.183      "z < z + $#(Suc(n))";
  12.184  by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
  12.185 -by (safe_tac intrel_cs);
  12.186 +by (safe_tac (!claset));
  12.187  by (simp_tac (!simpset addsimps [zadd, zminus]) 1);
  12.188  by (REPEAT_SOME (ares_tac [refl, exI, singletonI, ImageI, conjI, intrelI]));
  12.189  by (rtac le_less_trans 1);
  12.190 @@ -587,7 +590,7 @@
  12.191  qed "zless_zadd_Suc";
  12.192  
  12.193  goal Integ.thy "!!z1 z2 z3. [| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
  12.194 -by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc]));
  12.195 +by (safe_tac (!claset addSDs [zless_eq_zadd_Suc]));
  12.196  by (simp_tac 
  12.197      (!simpset addsimps [zadd_assoc, zless_zadd_Suc, znat_add RS sym]) 1);
  12.198  qed "zless_trans";
  12.199 @@ -599,9 +602,9 @@
  12.200  val zless_zsucI = zlessI RSN (2,zless_trans);
  12.201  
  12.202  goal Integ.thy "!!z w::int. z<w ==> ~w<z";
  12.203 -by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc]));
  12.204 +by (safe_tac (!claset addSDs [zless_eq_zadd_Suc]));
  12.205  by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
  12.206 -by (safe_tac intrel_cs);
  12.207 +by (safe_tac (!claset));
  12.208  by (asm_full_simp_tac (!simpset addsimps ([znat_def, zadd])) 1);
  12.209  by (asm_full_simp_tac
  12.210   (!simpset delsimps [add_Suc_right] addsimps [add_left_cancel, add_assoc, add_Suc_right RS sym]) 1);
  12.211 @@ -622,7 +625,7 @@
  12.212  bind_thm ("zless_irrefl", (zless_not_refl RS notE));
  12.213  
  12.214  goal Integ.thy "!!w. z<w ==> w ~= (z::int)";
  12.215 -by(fast_tac (HOL_cs addEs [zless_irrefl]) 1);
  12.216 +by(fast_tac (!claset addEs [zless_irrefl]) 1);
  12.217  qed "zless_not_refl2";
  12.218  
  12.219  
  12.220 @@ -631,7 +634,7 @@
  12.221      "z<w | z=w | w<(z::int)";
  12.222  by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
  12.223  by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
  12.224 -by (safe_tac intrel_cs);
  12.225 +by (safe_tac (!claset));
  12.226  by (asm_full_simp_tac
  12.227      (!simpset addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
  12.228  by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
  12.229 @@ -651,7 +654,7 @@
  12.230      "($#m < $#n) = (m<n)";
  12.231  by (simp_tac
  12.232      (!simpset addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
  12.233 -by (fast_tac (HOL_cs addIs [add_commute] addSEs [less_add_eq_less]) 1);
  12.234 +by (fast_tac (!claset addIs [add_commute] addSEs [less_add_eq_less]) 1);
  12.235  qed "zless_eq_less";
  12.236  
  12.237  goalw Integ.thy [zle_def, le_def] "($#m <= $#n) = (m<=n)";
  12.238 @@ -669,21 +672,21 @@
  12.239  val zleE = make_elim zleD;
  12.240  
  12.241  goalw Integ.thy [zle_def] "!!z. ~ z <= w ==> w<(z::int)";
  12.242 -by (fast_tac HOL_cs 1);
  12.243 +by (Fast_tac 1);
  12.244  qed "not_zleE";
  12.245  
  12.246  goalw Integ.thy [zle_def] "!!z. z < w ==> z <= (w::int)";
  12.247 -by (fast_tac (HOL_cs addEs [zless_asym]) 1);
  12.248 +by (fast_tac (!claset addEs [zless_asym]) 1);
  12.249  qed "zless_imp_zle";
  12.250  
  12.251  goalw Integ.thy [zle_def] "!!z. z <= w ==> z < w | z=(w::int)";
  12.252  by (cut_facts_tac [zless_linear] 1);
  12.253 -by (fast_tac (HOL_cs addEs [zless_irrefl,zless_asym]) 1);
  12.254 +by (fast_tac (!claset addEs [zless_irrefl,zless_asym]) 1);
  12.255  qed "zle_imp_zless_or_eq";
  12.256  
  12.257  goalw Integ.thy [zle_def] "!!z. z<w | z=w ==> z <=(w::int)";
  12.258  by (cut_facts_tac [zless_linear] 1);
  12.259 -by (fast_tac (HOL_cs addEs [zless_irrefl,zless_asym]) 1);
  12.260 +by (fast_tac (!claset addEs [zless_irrefl,zless_asym]) 1);
  12.261  qed "zless_or_eq_imp_zle";
  12.262  
  12.263  goal Integ.thy "(x <= (y::int)) = (x < y | x=y)";
  12.264 @@ -696,17 +699,17 @@
  12.265  
  12.266  val prems = goal Integ.thy "!!i. [| i <= j; j < k |] ==> i < (k::int)";
  12.267  by (dtac zle_imp_zless_or_eq 1);
  12.268 -by (fast_tac (HOL_cs addIs [zless_trans]) 1);
  12.269 +by (fast_tac (!claset addIs [zless_trans]) 1);
  12.270  qed "zle_zless_trans";
  12.271  
  12.272  goal Integ.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::int)";
  12.273  by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
  12.274 -            rtac zless_or_eq_imp_zle, fast_tac (HOL_cs addIs [zless_trans])]);
  12.275 +            rtac zless_or_eq_imp_zle, fast_tac (!claset addIs [zless_trans])]);
  12.276  qed "zle_trans";
  12.277  
  12.278  goal Integ.thy "!!z. [| z <= w; w <= z |] ==> z = (w::int)";
  12.279  by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
  12.280 -            fast_tac (HOL_cs addEs [zless_irrefl,zless_asym])]);
  12.281 +            fast_tac (!claset addEs [zless_irrefl,zless_asym])]);
  12.282  qed "zle_anti_sym";
  12.283  
  12.284  
  12.285 @@ -719,13 +722,13 @@
  12.286  (*** Monotonicity results ***)
  12.287  
  12.288  goal Integ.thy "!!v w z::int. v < w ==> v + z < w + z";
  12.289 -by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc]));
  12.290 +by (safe_tac (!claset addSDs [zless_eq_zadd_Suc]));
  12.291  by (simp_tac (!simpset addsimps zadd_ac) 1);
  12.292  by (simp_tac (!simpset addsimps [zadd_assoc RS sym, zless_zadd_Suc]) 1);
  12.293  qed "zadd_zless_mono1";
  12.294  
  12.295  goal Integ.thy "!!v w z::int. (v+z < w+z) = (v < w)";
  12.296 -by (safe_tac (HOL_cs addSEs [zadd_zless_mono1]));
  12.297 +by (safe_tac (!claset addSEs [zadd_zless_mono1]));
  12.298  by (dres_inst_tac [("z", "$~z")] zadd_zless_mono1 1);
  12.299  by (asm_full_simp_tac (!simpset addsimps [zadd_assoc]) 1);
  12.300  qed "zadd_left_cancel_zless";
    13.1 --- a/src/HOL/Lex/Auto.ML	Mon Jul 29 18:31:39 1996 +0200
    13.2 +++ b/src/HOL/Lex/Auto.ML	Tue Jul 30 17:33:26 1996 +0200
    13.3 @@ -24,16 +24,16 @@
    13.4  goalw Auto.thy [acc_prefix_def]
    13.5   "acc_prefix A s (x#xs) = (fin A (next A s x) | acc_prefix A (next A s x) xs)";
    13.6  by(simp_tac (!simpset addsimps [prefix_Cons]) 1);
    13.7 -by(safe_tac HOL_cs);
    13.8 +by(safe_tac (!claset));
    13.9    by(Asm_full_simp_tac 1);
   13.10    by (case_tac "zs=[]" 1);
   13.11     by(hyp_subst_tac 1);
   13.12     by(Asm_full_simp_tac 1);
   13.13 -  by(fast_tac (HOL_cs addSEs [Cons_neq_Nil]) 1);
   13.14 +  by(fast_tac (!claset addSEs [Cons_neq_Nil]) 1);
   13.15   by(res_inst_tac [("x","[x]")] exI 1);
   13.16   by(asm_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
   13.17  by(res_inst_tac [("x","x#us")] exI 1);
   13.18  by(Asm_simp_tac 1);
   13.19 -by (fast_tac HOL_cs 1);
   13.20 +by (Fast_tac 1);
   13.21  qed"acc_prefix_Cons";
   13.22  Addsimps [acc_prefix_Cons];
    14.1 --- a/src/HOL/Lex/AutoChopper.ML	Mon Jul 29 18:31:39 1996 +0200
    14.2 +++ b/src/HOL/Lex/AutoChopper.ML	Tue Jul 30 17:33:26 1996 +0200
    14.3 @@ -28,7 +28,7 @@
    14.4  by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
    14.5  by (strip_tac 1);
    14.6  by (rtac conjI 1);
    14.7 -by (fast_tac HOL_cs 1);
    14.8 +by (Fast_tac 1);
    14.9  by(simp_tac (!simpset addsimps [prefix_Cons] addcongs [conj_cong]) 1);
   14.10  by (strip_tac 1);
   14.11  by(REPEAT(eresolve_tac [conjE,exE] 1));
   14.12 @@ -36,13 +36,13 @@
   14.13  by (Simp_tac 1);
   14.14  by (case_tac "zsa = []" 1);
   14.15  by (Asm_simp_tac 1);
   14.16 -by (fast_tac HOL_cs 1);
   14.17 +by (Fast_tac 1);
   14.18  bind_thm("no_acc", result() RS spec RS spec RS mp);
   14.19  
   14.20  
   14.21  val [prem] = goal HOL.thy "? x.P(f(x)) ==> ? y.P(y)";
   14.22  by (cut_facts_tac [prem] 1);
   14.23 -by (fast_tac HOL_cs 1);
   14.24 +by (Fast_tac 1);
   14.25  val ex_special = result();
   14.26  
   14.27  
   14.28 @@ -59,7 +59,7 @@
   14.29  by (res_inst_tac[("xs","vss")] list_eq_cases 1);
   14.30   by(hyp_subst_tac 1);
   14.31   by(Simp_tac 1);
   14.32 - by (fast_tac (HOL_cs addSDs [no_acc]) 1);
   14.33 + by (fast_tac (!claset addSDs [no_acc]) 1);
   14.34  by(hyp_subst_tac 1);
   14.35  by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   14.36  val step2_a = (result() repeat_RS spec) RS mp;
   14.37 @@ -74,7 +74,7 @@
   14.38  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   14.39  by (list.induct_tac "xs" 1);
   14.40   by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   14.41 - by (fast_tac HOL_cs 1);
   14.42 + by (Fast_tac 1);
   14.43  by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   14.44  by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
   14.45  by(rename_tac "vss lrst" 1);  
   14.46 @@ -83,7 +83,7 @@
   14.47  by (case_tac "acc_prefix A (next A st a) list" 1);
   14.48   by(Asm_simp_tac 1);
   14.49  by (subgoal_tac "r @ [a] ~= []" 1);
   14.50 - by (fast_tac HOL_cs 1);
   14.51 + by (Fast_tac 1);
   14.52  by (Simp_tac 1);
   14.53  val step2_b = (result() repeat_RS spec) RS mp;
   14.54  
   14.55 @@ -97,7 +97,7 @@
   14.56  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   14.57  by (list.induct_tac "xs" 1);
   14.58   by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   14.59 - by (fast_tac HOL_cs 1);
   14.60 + by (Fast_tac 1);
   14.61  by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   14.62  by (strip_tac 1);
   14.63  by (rtac conjI 1);
   14.64 @@ -110,20 +110,20 @@
   14.65    by (Simp_tac 1);
   14.66    by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
   14.67     by (Simp_tac 1);
   14.68 -  by (fast_tac HOL_cs 1);
   14.69 +  by (Fast_tac 1);
   14.70   by (strip_tac 1);
   14.71   by (res_inst_tac [("x","[a]")] exI 1);
   14.72   by (Asm_simp_tac 1);
   14.73   by (subgoal_tac "r @ [a] ~= []" 1);
   14.74    br sym 1;
   14.75 -  by (fast_tac HOL_cs 1);
   14.76 +  by (Fast_tac 1);
   14.77   by (Simp_tac 1);
   14.78  by (strip_tac 1);
   14.79  by (res_inst_tac [("f","%k.a#k")] ex_special 1);
   14.80  by (Simp_tac 1);
   14.81  by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
   14.82   by (Simp_tac 1);
   14.83 -by (fast_tac HOL_cs 1);
   14.84 +by (Fast_tac 1);
   14.85  val step2_c = (result() repeat_RS spec) RS mp;
   14.86  
   14.87  
   14.88 @@ -136,7 +136,7 @@
   14.89  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   14.90  by (list.induct_tac "xs" 1);
   14.91   by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   14.92 - by (fast_tac HOL_cs 1);
   14.93 + by (Fast_tac 1);
   14.94  by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   14.95  by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
   14.96  by(rename_tac "vss lrst" 1);  
   14.97 @@ -147,7 +147,7 @@
   14.98  by (subgoal_tac "acc list (start A) [] [] ([],list) A = (yss,zs)" 1);
   14.99   by (Asm_simp_tac 2);
  14.100   by (subgoal_tac "r@[a] ~= []" 2);
  14.101 -  by (fast_tac HOL_cs 2);
  14.102 +  by (Fast_tac 2);
  14.103   by (Simp_tac 2);
  14.104  by (subgoal_tac "flat(yss) @ zs = list" 1);
  14.105   by(hyp_subst_tac 1);
  14.106 @@ -155,7 +155,7 @@
  14.107  by (case_tac "yss = []" 1);
  14.108   by (Asm_simp_tac 1);
  14.109   by (hyp_subst_tac 1);
  14.110 - by (fast_tac (HOL_cs addSDs [no_acc]) 1);
  14.111 + by (fast_tac (!claset addSDs [no_acc]) 1);
  14.112  by (etac ((neq_Nil_conv RS iffD1) RS exE) 1);
  14.113  by (etac exE 1);
  14.114  by (hyp_subst_tac 1);
  14.115 @@ -175,7 +175,7 @@
  14.116  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  14.117  by (list.induct_tac "xs" 1);
  14.118   by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
  14.119 - by (fast_tac HOL_cs 1);
  14.120 + by (Fast_tac 1);
  14.121  by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
  14.122  by (strip_tac 1);
  14.123  by (case_tac "acc_prefix A (next A st a) list" 1);
  14.124 @@ -207,13 +207,13 @@
  14.125  by (res_inst_tac [("x","[a]")] exI 1);
  14.126  by (rtac conjI 1);
  14.127   by (subgoal_tac "r @ [a] ~= []" 1);
  14.128 -  by (fast_tac HOL_cs 1);
  14.129 +  by (Fast_tac 1);
  14.130   by (Simp_tac 1);
  14.131  by (rtac list_cases 1);
  14.132   by (Simp_tac 1);
  14.133  by (asm_full_simp_tac (!simpset addsimps [acc_prefix_def] addcongs[conj_cong]) 1);
  14.134  by (etac thin_rl 1); (* speed up *)
  14.135 -by (fast_tac HOL_cs 1);
  14.136 +by (Fast_tac 1);
  14.137  val step2_e = (result() repeat_RS spec) RS mp;
  14.138  Addsimps[split_paired_All];
  14.139  
  14.140 @@ -228,7 +228,7 @@
  14.141   br mp 1;
  14.142    be step2_c 2;
  14.143   by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  14.144 - by (fast_tac HOL_cs 1);
  14.145 + by (Fast_tac 1);
  14.146  by (rtac conjI 1);
  14.147   by (asm_simp_tac (!simpset addsimps [step2_a] setloop (split_tac [expand_if])) 1);
  14.148  by (rtac conjI 1);
  14.149 @@ -238,5 +238,5 @@
  14.150  by (rtac mp 1);
  14.151   be step2_e 2;
  14.152   by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  14.153 -by (fast_tac HOL_cs 1);
  14.154 +by (Fast_tac 1);
  14.155  qed"auto_chopper_is_auto_chopper";
    15.1 --- a/src/HOL/Lex/Prefix.ML	Mon Jul 29 18:31:39 1996 +0200
    15.2 +++ b/src/HOL/Lex/Prefix.ML	Tue Jul 30 17:33:26 1996 +0200
    15.3 @@ -21,7 +21,7 @@
    15.4  goalw Prefix.thy [prefix_def] "(xs <= []) = (xs = [])";
    15.5  by (list.induct_tac "xs" 1);
    15.6  by (Simp_tac 1);
    15.7 -by (fast_tac HOL_cs 1);
    15.8 +by (Fast_tac 1);
    15.9  by (Simp_tac 1);
   15.10  qed "prefix_Nil";
   15.11  Addsimps [prefix_Nil];
   15.12 @@ -31,13 +31,13 @@
   15.13     "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
   15.14  by (list.induct_tac "xs" 1);
   15.15  by (Simp_tac 1);
   15.16 -by (fast_tac HOL_cs 1);
   15.17 +by (Fast_tac 1);
   15.18  by (Simp_tac 1);
   15.19 -by (fast_tac HOL_cs 1);
   15.20 +by (Fast_tac 1);
   15.21  qed "prefix_Cons";
   15.22  
   15.23  goalw Prefix.thy [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)";
   15.24  by(Simp_tac 1);
   15.25 -by (fast_tac HOL_cs 1);
   15.26 +by (Fast_tac 1);
   15.27  qed"Cons_prefix_Cons";
   15.28  Addsimps [Cons_prefix_Cons];