Classical tactics now use default claset.

--- a/src/HOL/IOA/ABP/Correctness.ML	Mon Jul 29 18:31:39 1996 +0200
+++ b/src/HOL/IOA/ABP/Correctness.ML	Tue Jul 30 17:33:26 1996 +0200
@@ -9,7 +9,7 @@
 open Impl; open Impl_finite;
 
 goal Abschannel.thy "(? x.x=P & Q(x)) = Q(P)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed"exis_elim";
 
 Delsimps [split_paired_All];
@@ -47,7 +47,7 @@
 goal Correctness.thy "(reduce(l)=[]) = (l=[])";  
  by (rtac iffI 1);
  by (subgoal_tac "(l~=[]) --> (reduce(l)~=[])" 1);
- by (fast_tac HOL_cs 1); 
+ by (Fast_tac 1); 
  by (List.list.induct_tac "l" 1);
  by (Simp_tac 1);
  by (Simp_tac 1);
@@ -139,7 +139,7 @@
 by (case_tac "list=[]" 1);
  by (asm_full_simp_tac (!simpset addsimps [reverse_Nil,reverse_Cons]) 1);
 by (rtac (expand_if RS ssubst) 1);
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
  by (rtac impI 1);
 by (Simp_tac 1);
 by (cut_inst_tac [("l","list")] cons_not_nil 1);
@@ -230,7 +230,7 @@
 by (TRY(
    (rtac conjI 1) THEN
 (* start states *)
-   (fast_tac set_cs 1)));
+   (Fast_tac 1)));
 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
@@ -246,7 +246,7 @@
 by (TRY(
    (rtac conjI 1) THEN
  (* start states *)
-   (fast_tac set_cs 1)));
+   (Fast_tac 1)));
 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
@@ -261,7 +261,7 @@
 by (TRY(
    (rtac conjI 1) THEN
 (* start states *)
-   (fast_tac set_cs 1)));
+   (Fast_tac 1)));
 (* main-part *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);

--- a/src/HOL/IOA/ABP/Lemmas.ML	Mon Jul 29 18:31:39 1996 +0200
+++ b/src/HOL/IOA/ABP/Lemmas.ML	Tue Jul 30 17:33:26 1996 +0200
@@ -8,22 +8,22 @@
 (* Logic *)
 
 val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
-  by(fast_tac (HOL_cs addDs prems) 1);
+  by(fast_tac (!claset addDs prems) 1);
 qed "imp_conj_lemma";
 
 goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 val and_de_morgan_and_absorbe = result();
 
 goal HOL.thy "(if C then A else B) --> (A|B)";
 by (rtac (expand_if RS ssubst) 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 val bool_if_impl_or = result();
 
 (* Sets *)
 
 val set_lemmas =
-   map (fn s => prove_goal Set.thy s (fn _ => [fast_tac set_cs 1]))
+   map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1]))
         ["f(x) : (UN x. {f(x)})",
          "f x y : (UN x y. {f x y})",
          "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})",
@@ -33,11 +33,11 @@
    namely for Intersections and the empty list (compatibility of IOA!)  *)
 goal Set.thy "(UN b.{x.x=f(b)})= (UN b.{f(b)})"; 
  by (rtac set_ext 1);
- by (fast_tac set_cs 1);
+ by (Fast_tac 1);
 val singleton_set =result();
 
 goal HOL.thy "((A|B)=False) = ((~A)&(~B))";
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 val de_morgan = result();
 
 (* Lists *)
@@ -53,5 +53,5 @@
 goal List.thy "l ~= [] --> (? x xs. l = (x#xs))";
  by (List.list.induct_tac "l" 1);
  by (simp_tac list_ss 1);
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 qed"cons_not_nil";

--- a/src/HOL/IOA/NTP/Correctness.ML	Mon Jul 29 18:31:39 1996 +0200
+++ b/src/HOL/IOA/NTP/Correctness.ML	Tue Jul 30 17:33:26 1996 +0200
@@ -106,7 +106,7 @@
 by(case_tac "sq(sen(s))=[]" 1);
 
 by(asm_full_simp_tac ss' 1);
-by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1);
+by(fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
 
 by(case_tac "m = hd(sq(sen(s)))" 1);
 
@@ -114,7 +114,7 @@
                      [imp_ex_equiv,neq_Nil_conv,ex_all_equiv]) 1);
 
 by(Asm_full_simp_tac 1);
-by(fast_tac (HOL_cs addSDs [add_leD1 RS leD]) 1);
+by(fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
 
 by(Asm_full_simp_tac 1);
 qed"ntp_correct";

--- a/src/HOL/IOA/NTP/Impl.ML	Mon Jul 29 18:31:39 1996 +0200
+++ b/src/HOL/IOA/NTP/Impl.ML	Tue Jul 30 17:33:26 1996 +0200
@@ -182,14 +182,14 @@
   by (forward_tac [rewrite_rule [Impl.inv1_def]
                                 (inv1 RS invariantE) RS conjunct1] 1);
   by (tac2 1);
-  by (fast_tac (HOL_cs addDs [add_leD1,leD]) 1);
+  by (fast_tac (!claset addDs [add_leD1,leD]) 1);
 
   (* 3 *)
   by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1);
 
   by (tac2 1);
   by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]);
-  by (fast_tac (HOL_cs addDs [add_leD1,leD]) 1);
+  by (fast_tac (!claset addDs [add_leD1,leD]) 1);
 
   (* 2 *)
   by (tac2 1);
@@ -245,7 +245,7 @@
   (* 7 *)
   by (tac3 1);
   by (tac_ren 1);
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
 
   (* 6 - 3 *)
 

--- a/src/HOL/IOA/NTP/Lemmas.ML	Mon Jul 29 18:31:39 1996 +0200
+++ b/src/HOL/IOA/NTP/Lemmas.ML	Tue Jul 30 17:33:26 1996 +0200
@@ -10,43 +10,43 @@
 
 (* Logic *)
 val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
-  by(fast_tac (HOL_cs addDs prems) 1);
+  by(fast_tac (!claset addDs prems) 1);
 qed "imp_conj_lemma";
 
 goal HOL.thy "(P --> (? x. Q(x))) = (? x. P --> Q(x))";
-  by(fast_tac HOL_cs 1);
+  by(Fast_tac 1);
 qed "imp_ex_equiv";
 
 goal HOL.thy "(A --> B & C) = ((A --> B) & (A --> C))";
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
 qed "fork_lemma";
 
 goal HOL.thy "((A --> B) & (C --> B)) = ((A | C) --> B)";
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
 qed "imp_or_lem";
 
 goal HOL.thy "(X = (~ Y)) = ((~X) = Y)";
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
 qed "neg_flip";
 
 goal HOL.thy "P --> Q(M) --> Q(if P then M else N)";
   by (rtac impI 1); 
   by (rtac impI 1);
   by (rtac (expand_if RS iffD2) 1);
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
 qed "imp_true_decompose";
 
 goal HOL.thy "(~P) --> Q(N) --> Q(if P then M else N)";
   by (rtac impI 1); 
   by (rtac impI 1);
   by (rtac (expand_if RS iffD2) 1);
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
 qed "imp_false_decompose";
 
 
 (* Sets *)
 val set_lemmas =
-   map (fn s => prove_goal Set.thy s (fn _ => [fast_tac set_cs 1]))
+   map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1]))
         ["f(x) : (UN x. {f(x)})",
          "f x y : (UN x y. {f x y})",
          "!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})",
@@ -75,7 +75,7 @@
   by (nat_ind_tac "x" 1);
   by (Simp_tac 1);
   by (Asm_simp_tac 1);
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
 qed "nonzero_is_succ";
 
 goal Arith.thy "(m::nat) < n --> m + p < n + p";
@@ -96,7 +96,7 @@
   by (Asm_simp_tac 1);
   by (rtac impI 1);
   by (dtac Suc_leD 1);
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
 qed "left_add_leq";
 
 goal Arith.thy "(A::nat) < B --> C < D --> A + C < B + D";
@@ -115,7 +115,7 @@
   by (rtac impI 1);
   by (rtac impI 1);
   by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
-  by (safe_tac HOL_cs);
+  by (safe_tac (!claset));
   by (rtac (less_add_cong RS mp RS mp) 1);
   by (assume_tac 1);
   by (assume_tac 1);
@@ -143,21 +143,21 @@
   by (Simp_tac 1);
   by (rtac iffI 1);
   by (Asm_full_simp_tac 1);
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
 qed "suc_not_zero";
 
 goal Arith.thy "Suc(x) <= y --> (? z. y = Suc(z))";
   by (rtac impI 1);
   by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
-  by (safe_tac HOL_cs);
-  by (fast_tac HOL_cs 2);
+  by (safe_tac (!claset));
+  by (Fast_tac 2);
   by (asm_simp_tac (!simpset addsimps [suc_not_zero]) 1);
 qed "suc_leq_suc";
 
 goal Arith.thy "~0<n --> n = 0";
   by (nat_ind_tac "n" 1);
   by (Asm_simp_tac 1);
-  by (safe_tac HOL_cs);
+  by (safe_tac (!claset));
   by (Asm_full_simp_tac 1);
   by (Asm_full_simp_tac 1);
 qed "zero_eq";
@@ -165,7 +165,7 @@
 goal Arith.thy "x < Suc(y) --> x<=y";
   by (nat_ind_tac "n" 1);
   by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
-  by (safe_tac HOL_cs);
+  by (safe_tac (!claset));
   by (etac less_imp_le 1);
 qed "less_suc_imp_leq";
 

--- a/src/HOL/IOA/NTP/Multiset.ML	Mon Jul 29 18:31:39 1996 +0200
+++ b/src/HOL/IOA/NTP/Multiset.ML	Tue Jul 30 17:33:26 1996 +0200
@@ -34,7 +34,7 @@
                          addsimps [Multiset.delm_nonempty_def,
                                    Multiset.countm_nonempty_def]
                          setloop (split_tac [expand_if])) 1);
-  by (safe_tac HOL_cs);
+  by (safe_tac (!claset));
   by (Asm_full_simp_tac 1);
 qed "count_delm_simp";
 

--- a/src/HOL/IOA/meta_theory/IOA.ML	Mon Jul 29 18:31:39 1996 +0200
+++ b/src/HOL/IOA/meta_theory/IOA.ML	Tue Jul 30 17:33:26 1996 +0200
@@ -41,7 +41,7 @@
 \   (s(n)=Some(a) & a : externals(asig_of(A)))";
   by (Option.option.induct_tac "s(n)" 1);
   by (ALLGOALS (simp_tac (!simpset setloop (split_tac [expand_if]))));
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
 qed "mk_trace_thm";
 
 goalw IOA.thy [reachable_def] "!!A. s:starts_of(A) ==> reachable A s";
@@ -53,7 +53,7 @@
 goalw IOA.thy (reachable_def::exec_rws)
 "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t";
   by(Asm_full_simp_tac 1);
-  by(safe_tac set_cs);
+  by(safe_tac (!claset));
   by(res_inst_tac [("x","(%i.if i<n then fst ex i                    \
 \                            else (if i=n then Some a else None),    \
 \                         %i.if i<Suc n then snd ex i else t)")] bexI 1);
@@ -66,7 +66,7 @@
   by(asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   be disjE 1;
   by(Asm_simp_tac 1);
-  by(fast_tac HOL_cs 1);
+  by(Fast_tac 1);
   by(forward_tac [less_not_sym] 1);
   by(asm_simp_tac (!simpset addsimps [less_not_refl2,less_Suc_eq]) 1);
 qed "reachable_n";
@@ -76,16 +76,16 @@
 \     !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \
 \  ==> invariant A P";
   by (rewrite_goals_tac(reachable_def::Let_def::exec_rws));
-  by (safe_tac set_cs);
+  by (safe_tac (!claset));
   by (res_inst_tac [("Q","reachable A (snd ex n)")] conjunct1 1);
   by (nat_ind_tac "n" 1);
-  by (fast_tac (set_cs addIs [p1,reachable_0]) 1);
+  by (fast_tac (!claset addIs [p1,reachable_0]) 1);
   by (eres_inst_tac[("x","n1")]allE 1);
   by (eres_inst_tac[("P","%x.!a.?Q x a"), ("opt","fst ex n1")] optE 1);
   by (Asm_simp_tac 1);
-  by (safe_tac HOL_cs);
+  by (safe_tac (!claset));
   by (etac (p2 RS mp) 1);
-  by (ALLGOALS(fast_tac(set_cs addDs [hd Option.option.inject RS iffD1,
+  by (ALLGOALS(fast_tac(!claset addDs [hd Option.option.inject RS iffD1,
                                       reachable_n])));
 qed "invariantI";
 
@@ -93,7 +93,7 @@
  "[| !!s. s : starts_of(A) ==> P(s); \
 \   !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
 \ |] ==> invariant A P";
-  by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1);
+  by (fast_tac (!claset addSIs [invariantI] addSDs [p1,p2]) 1);
 qed "invariantI1";
 
 val [p1,p2] = goalw IOA.thy [invariant_def]
@@ -116,7 +116,7 @@
 (* Every state in an execution is reachable *)
 goalw IOA.thy [reachable_def] 
 "!!A. ex:executions(A) ==> !n. reachable A (snd ex n)";
-  by (fast_tac set_cs 1);
+  by (Fast_tac 1);
 qed "states_of_exec_reachable";
 
 
@@ -155,19 +155,19 @@
 \  (externals(asig_of(A1)) Un externals(asig_of(A2)))";
 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);
 by (rtac set_ext 1); 
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed"externals_of_par"; 
 
 goalw IOA.thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
  "!! a. [| compat_ioas A1 A2; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))";
 by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (best_tac (!claset addEs [equalityCE]) 1);
 qed"ext1_is_not_int2";
 
 goalw IOA.thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
  "!! a. [| compat_ioas A2 A1 ; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))";
 by (Asm_full_simp_tac 1);
-by (best_tac (set_cs addEs [equalityCE]) 1);
+by (best_tac (!claset addEs [equalityCE]) 1);
 qed"ext2_is_not_int1";
 
 val ext1_ext2_is_not_act2 = ext1_is_not_int2 RS int_and_ext_is_act;

--- a/src/HOL/IOA/meta_theory/Option.ML	Mon Jul 29 18:31:39 1996 +0200
+++ b/src/HOL/IOA/meta_theory/Option.ML	Tue Jul 30 17:33:26 1996 +0200
@@ -11,7 +11,7 @@
 val [prem] = goal Option.thy "P(opt) ==> P(None) | (? x. P(Some(x)))";
  br (prem RS rev_mp) 1;
  by (Option.option.induct_tac "opt" 1);
- by (ALLGOALS(fast_tac HOL_cs));
+ by (ALLGOALS(Fast_tac));
 val optE = store_thm("optE", standard(result() RS disjE));
 
 goal Option.thy "x=None | (? y.x=Some(y))"; 

--- a/src/HOL/IOA/meta_theory/Solve.ML	Mon Jul 29 18:31:39 1996 +0200
+++ b/src/HOL/IOA/meta_theory/Solve.ML	Tue Jul 30 17:33:26 1996 +0200
@@ -15,7 +15,7 @@
 \          is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
 
   by (simp_tac(!simpset addsimps [has_trace_def])1);
-  by (safe_tac set_cs);
+  by (safe_tac (!claset));
 
   (* choose same trace, therefore same NF *)
   by (res_inst_tac[("x","mk_trace  C (fst ex)")] exI 1);
@@ -32,7 +32,7 @@
 
   (* Now show that it's an execution *)
   by (asm_full_simp_tac(!simpset addsimps [executions_def]) 1);
-  by (safe_tac set_cs);
+  by (safe_tac (!claset));
 
   (* Start states map to start states *)
   by (dtac bspec 1);
@@ -40,7 +40,7 @@
 
   (* Show that it's an execution fragment *)
   by (asm_full_simp_tac (!simpset addsimps [is_execution_fragment_def])1);
-  by (safe_tac HOL_cs);
+  by (safe_tac (!claset));
 
   by (eres_inst_tac [("x","snd ex n")] allE 1);
   by (eres_inst_tac [("x","snd ex (Suc n)")] allE 1);
@@ -51,7 +51,7 @@
 (* Lemmata *)
 
 val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
-  by(fast_tac (HOL_cs addDs prems) 1);
+  by(fast_tac (!claset addDs prems) 1);
 val imp_conj_lemma = result();
 
 
@@ -61,7 +61,7 @@
 \  a:externals(asig_of(A1)) & a~:externals(asig_of(A2)) |  \
 \  a~:externals(asig_of(A1)) & a:externals(asig_of(A2)))";
 by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_of_par,asig_comp_def,asig_inputs_def,asig_outputs_def]) 1);
- by (fast_tac set_cs 1);
+ by (Fast_tac 1);
 val externals_of_par_extra = result(); 
 
 goal Solve.thy "!!s.[| reachable (C1||C2) s |] ==> reachable C1 (fst s)";
@@ -73,7 +73,7 @@
 \    %i.fst (snd ex i))")]  bexI 1);
 (* fst(s) is in projected execution *)
  by (Simp_tac 1);
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 (* projected execution is indeed an execution *)
 by (asm_full_simp_tac (!simpset addsimps [executions_def,is_execution_fragment_def,
     par_def, starts_of_def,trans_of_def]) 1);
@@ -108,7 +108,7 @@
 \    %i.snd (snd ex i))")]  bexI 1);
 (* fst(s) is in projected execution *)
  by (Simp_tac 1);
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 (* projected execution is indeed an execution *)
  by (asm_full_simp_tac (!simpset addsimps [executions_def,is_execution_fragment_def,
     par_def, starts_of_def,trans_of_def]) 1);
@@ -138,7 +138,7 @@
  by (rtac conjI 1);
 (* start_states *)
  by (asm_full_simp_tac (!simpset addsimps [par_def, starts_of_def]) 1);
- by (fast_tac set_cs 1);
+ by (Fast_tac 1);
 (* transitions *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
@@ -165,7 +165,7 @@
 by (subgoal_tac "a~:externals(asig_of(A1)) & a~:externals(asig_of(A2))" 1);
 (* delete auxiliary subgoal *)
 by (Asm_full_simp_tac 2);
-by (fast_tac HOL_cs 2);
+by (Fast_tac 2);
 by (simp_tac (!simpset addsimps [conj_disj_distribR] addcongs [conj_cong]
                  setloop (split_tac [expand_if])) 1);
 by(REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
@@ -202,19 +202,19 @@
 by (dtac sym 1);
 by (dtac sym 1);
 by (Asm_full_simp_tac 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
 qed"reachable_rename_ioa";
 
 
 (* HOL Lemmata - must already exist ! *)
 goal HOL.thy  "(~(A|B)) =(~A&~B)";
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 val disj_demorgan = result();
 goal HOL.thy  "(~(A&B)) =(~A|~B)";
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 val conj_demorgan = result();
 goal HOL.thy  "(~(? x.P x)) =(! x. (~ (P x)))";
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 val neg_ex = result();
 
 
@@ -227,7 +227,7 @@
 by (rtac imp_conj_lemma 1);
 by (simp_tac (!simpset addsimps [rename_def]) 1);
 by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
 by (rtac (expand_if RS ssubst) 1);
  by (rtac conjI 1);
  by (rtac impI 1);

--- a/src/HOL/Integ/Bin.ML	Mon Jul 29 18:31:39 1996 +0200
+++ b/src/HOL/Integ/Bin.ML	Tue Jul 30 17:33:26 1996 +0200
@@ -54,7 +54,7 @@
 
 (* SHOULD THIS THEOREM BE ADDED TO HOL_SS ? *)
 val my = prove_goal HOL.thy "(False = (~P)) = P"
-	(fn prem => [(fast_tac HOL_cs 1)]);
+	(fn prem => [(Fast_tac 1)]);
 
 qed_goal "bin_add_Bcons_Bcons0" Bin.thy "bin_add (Bcons v False) (Bcons w y) = norm_Bcons (bin_add v w) y"
 	(fn prem => [(simp_tac (!simpset addsimps [my]) 1)]);
@@ -141,7 +141,7 @@
 
 goal Bin.thy "integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
 by (cut_facts_tac [integ_of_bin_add_lemma] 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "integ_of_bin_add";
 
 val bin_mult_simps = [integ_of_bin_minus, integ_of_bin_add,integ_of_bin_norm_Bcons];

--- a/src/HOL/Integ/Equiv.ML	Mon Jul 29 18:31:39 1996 +0200
+++ b/src/HOL/Integ/Equiv.ML	Tue Jul 30 17:33:26 1996 +0200
@@ -10,18 +10,20 @@
 
 open Equiv;
 
+Delrules [equalityI];
+
 (*** Suppes, Theorem 70: r is an equiv relation iff converse(r) O r = r ***)
 
 (** first half: equiv A r ==> converse(r) O r = r **)
 
 goalw Equiv.thy [trans_def,sym_def,converse_def]
     "!!r. [| sym(r); trans(r) |] ==> converse(r) O r <= r";
-by (fast_tac (comp_cs addSEs [converseD]) 1);
+by (fast_tac (!claset addSEs [converseD]) 1);
 qed "sym_trans_comp_subset";
 
 goalw Equiv.thy [refl_def]
     "!!A r. refl A r ==> r <= converse(r) O r";
-by (fast_tac (rel_cs addIs [compI]) 1);
+by (fast_tac (!claset addIs [compI]) 1);
 qed "refl_comp_subset";
 
 goalw Equiv.thy [equiv_def]
@@ -36,9 +38,9 @@
     "!!A r. [| converse(r) O r = r;  Domain(r) = A |] ==> equiv A r";
 by (etac equalityE 1);
 by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1);
-by (safe_tac set_cs);
-by (fast_tac (set_cs addSIs [converseI] addIs [compI]) 3);
-by (ALLGOALS (fast_tac (rel_cs addIs [compI] addSEs [compE])));
+by (safe_tac (!claset));
+by (fast_tac (!claset addSIs [converseI] addIs [compI]) 3);
+by (ALLGOALS (fast_tac (!claset addIs [compI] addSEs [compE])));
 qed "comp_equivI";
 
 (** Equivalence classes **)
@@ -46,28 +48,28 @@
 (*Lemma for the next result*)
 goalw Equiv.thy [equiv_def,trans_def,sym_def]
     "!!A r. [| equiv A r;  (a,b): r |] ==> r^^{a} <= r^^{b}";
-by (safe_tac rel_cs);
+by (safe_tac (!claset));
 by (rtac ImageI 1);
-by (fast_tac rel_cs 2);
-by (fast_tac rel_cs 1);
+by (Fast_tac 2);
+by (Fast_tac 1);
 qed "equiv_class_subset";
 
 goal Equiv.thy "!!A r. [| equiv A r;  (a,b): r |] ==> r^^{a} = r^^{b}";
 by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1));
 by (rewrite_goals_tac [equiv_def,sym_def]);
-by (fast_tac rel_cs 1);
+by (Fast_tac 1);
 qed "equiv_class_eq";
 
 val prems = goalw Equiv.thy [equiv_def,refl_def]
     "[| equiv A r;  a: A |] ==> a: r^^{a}";
 by (cut_facts_tac prems 1);
-by (fast_tac rel_cs 1);
+by (Fast_tac 1);
 qed "equiv_class_self";
 
 (*Lemma for the next result*)
 goalw Equiv.thy [equiv_def,refl_def]
     "!!A r. [| equiv A r;  r^^{b} <= r^^{a};  b: A |] ==> (a,b): r";
-by (fast_tac rel_cs 1);
+by (Fast_tac 1);
 qed "subset_equiv_class";
 
 val prems = goal Equiv.thy
@@ -78,7 +80,7 @@
 (*thus r^^{a} = r^^{b} as well*)
 goalw Equiv.thy [equiv_def,trans_def,sym_def]
     "!!A r. [| equiv A r;  x: (r^^{a} Int r^^{b}) |] ==> (a,b): r";
-by (fast_tac rel_cs 1);
+by (Fast_tac 1);
 qed "equiv_class_nondisjoint";
 
 val [major] = goalw Equiv.thy [equiv_def,refl_def]
@@ -88,7 +90,7 @@
 
 goal Equiv.thy
     "!!A r. equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
-by (safe_tac rel_cs);
+by (safe_tac (!claset));
 by ((rtac equiv_class_eq 1) THEN (assume_tac 1) THEN (assume_tac 1));
 by ((rtac eq_equiv_class 3) THEN 
     (assume_tac 4) THEN (assume_tac 4) THEN (assume_tac 3));
@@ -100,7 +102,7 @@
 
 goal Equiv.thy
     "!!A r. [| equiv A r;  x: A;  y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
-by (safe_tac rel_cs);
+by (safe_tac (!claset));
 by ((rtac eq_equiv_class 1) THEN 
     (assume_tac 1) THEN (assume_tac 1) THEN (assume_tac 1));
 by ((rtac equiv_class_eq 1) THEN 
@@ -123,7 +125,7 @@
 by (resolve_tac [major RS UN_E] 1);
 by (rtac minor 1);
 by (assume_tac 2);
-by (fast_tac rel_cs 1);
+by (Fast_tac 1);
 qed "quotientE";
 
 (** Not needed by Theory Integ --> bypassed **)
@@ -136,10 +138,10 @@
 (** Not needed by Theory Integ --> bypassed **)
 (*goalw Equiv.thy [quotient_def]
     "!!A r. [| equiv A r;  X: A/r;  Y: A/r |] ==> X=Y | (X Int Y <= 0)";
-by (safe_tac (ZF_cs addSIs [equiv_class_eq]));
+by (safe_tac (!claset addSIs [equiv_class_eq]));
 by (assume_tac 1);
 by (rewrite_goals_tac [equiv_def,trans_def,sym_def]);
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
 qed "quotient_disj";
 **)
 
@@ -147,7 +149,7 @@
 
 (* theorem needed to prove UN_equiv_class *)
 goal Set.thy "!!A. [| a:A; ! y:A. b(y)=b(a) |] ==> (UN y:A. b(y))=b(a)";
-by (fast_tac (!claset addSEs [equalityE]) 1);
+by (fast_tac (!claset addSEs [equalityE] addSIs [equalityI]) 1);
 qed "UN_singleton_lemma";
 val UN_singleton = ballI RSN (2,UN_singleton_lemma);
 
@@ -165,7 +167,7 @@
 by (assume_tac 1);
 by (assume_tac 1);
 by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]);
-by (fast_tac rel_cs 1);
+by (Fast_tac 1);
 qed "UN_equiv_class";
 
 (*Resolve th against the "local" premises*)
@@ -177,7 +179,7 @@
 \       !!x.  x : A ==> b(x) : B |]     \
 \    ==> (UN x:X. b(x)) : B";
 by (cut_facts_tac prems 1);
-by (safe_tac rel_cs);
+by (safe_tac (!claset));
 by (rtac (localize UN_equiv_class RS ssubst) 1);
 by (REPEAT (ares_tac prems 1));
 qed "UN_equiv_class_type";
@@ -191,7 +193,7 @@
 \       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |]         \
 \    ==> X=Y";
 by (cut_facts_tac prems 1);
-by (safe_tac rel_cs);
+by (safe_tac ((!claset) delrules [equalityI]));
 by (rtac (equivA RS equiv_class_eq) 1);
 by (REPEAT (ares_tac prems 1));
 by (etac box_equals 1);
@@ -204,20 +206,20 @@
 
 goalw Equiv.thy [congruent_def,congruent2_def,equiv_def,refl_def]
     "!!A r. [| equiv A r;  congruent2 r b;  a: A |] ==> congruent r (b a)";
-by (fast_tac rel_cs 1);
+by (Fast_tac 1);
 qed "congruent2_implies_congruent";
 
 val equivA::prems = goalw Equiv.thy [congruent_def]
     "[| equiv A r;  congruent2 r b;  a: A |] ==> \
 \    congruent r (%x1. UN x2:r^^{a}. b x1 x2)";
 by (cut_facts_tac (equivA::prems) 1);
-by (safe_tac rel_cs);
+by (safe_tac (!claset));
 by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
 by (assume_tac 1);
 by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class,
                                      congruent2_implies_congruent]) 1);
 by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
-by (fast_tac rel_cs 1);
+by (Fast_tac 1);
 qed "congruent2_implies_congruent_UN";
 
 val prems as equivA::_ = goal Equiv.thy
@@ -236,7 +238,7 @@
 \       !!x1 x2.  [| x1: A; x2: A |] ==> b x1 x2 : B |]    \
 \    ==> (UN x1:X1. UN x2:X2. b x1 x2) : B";
 by (cut_facts_tac prems 1);
-by (safe_tac rel_cs);
+by (safe_tac (!claset));
 by (REPEAT (ares_tac (prems@[UN_equiv_class_type,
                              congruent2_implies_congruent_UN,
                              congruent2_implies_congruent, quotientI]) 1));
@@ -251,7 +253,7 @@
 \       !! y z w. [| w: A;  (y,z) : r |] ==> b w y = b w z       \
 \    |] ==> congruent2 r b";
 by (cut_facts_tac prems 1);
-by (safe_tac rel_cs);
+by (safe_tac (!claset));
 by (rtac trans 1);
 by (REPEAT (ares_tac prems 1
      ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1));

--- a/src/HOL/Integ/Integ.ML	Mon Jul 29 18:31:39 1996 +0200
+++ b/src/HOL/Integ/Integ.ML	Tue Jul 30 17:33:26 1996 +0200
@@ -16,6 +16,8 @@
 
 open Integ;
 
+Delrules [equalityI];
+
 
 (*** Proving that intrel is an equivalence relation ***)
 
@@ -35,14 +37,14 @@
 val prems = goalw Integ.thy [intrel_def]
     "[| x1+y2 = x2+y1|] ==> \
 \    ((x1,y1),(x2,y2)): intrel";
-by (fast_tac (rel_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
 qed "intrelI";
 
 (*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
 goalw Integ.thy [intrel_def]
   "p: intrel --> (EX x1 y1 x2 y2. \
 \                  p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1)";
-by (fast_tac rel_cs 1);
+by (Fast_tac 1);
 qed "intrelE_lemma";
 
 val [major,minor] = goal Integ.thy
@@ -53,10 +55,11 @@
 by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
 qed "intrelE";
 
-val intrel_cs = rel_cs addSIs [intrelI] addSEs [intrelE];
+AddSIs [intrelI];
+AddSEs [intrelE];
 
 goal Integ.thy "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)";
-by (fast_tac intrel_cs 1);
+by (Fast_tac 1);
 qed "intrel_iff";
 
 goal Integ.thy "(x,x): intrel";
@@ -65,7 +68,7 @@
 
 goalw Integ.thy [equiv_def, refl_def, sym_def, trans_def]
     "equiv {x::(nat*nat).True} intrel";
-by (fast_tac (intrel_cs addSIs [intrel_refl] 
+by (fast_tac (!claset addSIs [intrel_refl] 
                         addSEs [sym, integ_trans_lemma]) 1);
 qed "equiv_intrel";
 
@@ -75,7 +78,7 @@
     (equiv_intrel RS eq_equiv_class_iff));
 
 goalw Integ.thy  [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "intrel_in_integ";
 
 goal Integ.thy "inj_onto Abs_Integ Integ";
@@ -103,8 +106,8 @@
 by (REPEAT (rtac intrel_in_integ 1));
 by (dtac eq_equiv_class 1);
 by (rtac equiv_intrel 1);
-by (fast_tac set_cs 1);
-by (safe_tac intrel_cs);
+by (Fast_tac 1);
+by (safe_tac (!claset));
 by (Asm_full_simp_tac 1);
 qed "inj_znat";
 
@@ -113,7 +116,7 @@
 
 goalw Integ.thy [congruent_def]
   "congruent intrel (%p. split (%x y. intrel^^{(y,x)}) p)";
-by (safe_tac intrel_cs);
+by (safe_tac (!claset));
 by (asm_simp_tac (!simpset addsimps add_ac) 1);
 qed "zminus_congruent";
 
@@ -168,12 +171,12 @@
 goalw Integ.thy [znegative_def, znat_def]
     "~ znegative($# n)";
 by (Simp_tac 1);
-by (safe_tac intrel_cs);
+by (safe_tac (!claset));
 by (rtac ccontr 1);
 by (etac notE 1);
 by (Asm_full_simp_tac 1);
 by (dtac not_znegative_znat_lemma 1);
-by (fast_tac (HOL_cs addDs [leD]) 1);
+by (fast_tac (!claset addDs [leD]) 1);
 qed "not_znegative_znat";
 
 goalw Integ.thy [znegative_def, znat_def] "znegative($~ $# Suc(n))";
@@ -200,7 +203,7 @@
 
 goalw Integ.thy [congruent_def]
     "congruent intrel (split (%x y. intrel^^{((y-x) + (x-(y::nat)),0)}))";
-by (safe_tac intrel_cs);
+by (safe_tac (!claset));
 by (Asm_simp_tac 1);
 by (etac rev_mp 1);
 by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1);
@@ -245,7 +248,7 @@
     "congruent2 intrel (%p1 p2.                  \
 \         split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)";
 (*Proof via congruent2_commuteI seems longer*)
-by (safe_tac intrel_cs);
+by (safe_tac (!claset));
 by (asm_simp_tac (!simpset addsimps [add_assoc]) 1);
 (*The rest should be trivial, but rearranging terms is hard*)
 by (res_inst_tac [("x1","x1a")] (add_left_commute RS ssubst) 1);
@@ -332,7 +335,7 @@
 \               split (%x1 y1. split (%x2 y2.   \
 \                   intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
 by (rtac (equiv_intrel RS congruent2_commuteI) 1);
-by (safe_tac intrel_cs);
+by (safe_tac (!claset));
 by (rewtac split_def);
 by (simp_tac (!simpset addsimps add_ac@mult_ac) 1);
 by (asm_simp_tac (!simpset delsimps [equiv_intrel_iff]
@@ -466,31 +469,31 @@
 qed "zsuc_zpred";
 
 goal Integ.thy "(zpred(z)=w) = (z=zsuc(w))";
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
 by (rtac (zsuc_zpred RS sym) 1);
 by (rtac zpred_zsuc 1);
 qed "zpred_to_zsuc";
 
 goal Integ.thy "(zsuc(z)=w)=(z=zpred(w))";
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
 by (rtac (zpred_zsuc RS sym) 1);
 by (rtac zsuc_zpred 1);
 qed "zsuc_to_zpred";
 
 goal Integ.thy "($~ z = w) = (z = $~ w)";
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
 by (rtac (zminus_zminus RS sym) 1);
 by (rtac zminus_zminus 1);
 qed "zminus_exchange";
 
 goal Integ.thy"(zsuc(z)=zsuc(w)) = (z=w)";
-by (safe_tac intrel_cs);
+by (safe_tac (!claset));
 by (dres_inst_tac [("f","zpred")] arg_cong 1);
 by (asm_full_simp_tac (!simpset addsimps [zpred_zsuc]) 1);
 qed "bijective_zsuc";
 
 goal Integ.thy"(zpred(z)=zpred(w)) = (z=w)";
-by (safe_tac intrel_cs);
+by (safe_tac (!claset));
 by (dres_inst_tac [("f","zsuc")] arg_cong 1);
 by (asm_full_simp_tac (!simpset addsimps [zsuc_zpred]) 1);
 qed "bijective_zpred";
@@ -549,7 +552,7 @@
 val zsuc_n_not_n = n_not_zsuc_n RS not_sym;
 
 goal Integ.thy "w ~= zpred(w)";
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
 by (dres_inst_tac [("x","w"),("f","zsuc")] arg_cong 1);
 by (asm_full_simp_tac (!simpset addsimps [zsuc_zpred,zsuc_n_not_n]) 1);
 qed "n_not_zpred_n";
@@ -563,9 +566,9 @@
     "!!w. w<z ==> ? n. z = w + $#(Suc(n))";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-by (safe_tac intrel_cs);
+by (safe_tac (!claset));
 by (asm_full_simp_tac (!simpset addsimps [zadd, zminus]) 1);
-by (safe_tac (intrel_cs addSDs [less_eq_Suc_add]));
+by (safe_tac (!claset addSDs [less_eq_Suc_add]));
 by (res_inst_tac [("x","k")] exI 1);
 by (asm_full_simp_tac (!simpset delsimps [add_Suc, add_Suc_right]
                                 addsimps ([add_Suc RS sym] @ add_ac)) 1);
@@ -578,7 +581,7 @@
 goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] 
     "z < z + $#(Suc(n))";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (safe_tac intrel_cs);
+by (safe_tac (!claset));
 by (simp_tac (!simpset addsimps [zadd, zminus]) 1);
 by (REPEAT_SOME (ares_tac [refl, exI, singletonI, ImageI, conjI, intrelI]));
 by (rtac le_less_trans 1);
@@ -587,7 +590,7 @@
 qed "zless_zadd_Suc";
 
 goal Integ.thy "!!z1 z2 z3. [| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
-by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc]));
+by (safe_tac (!claset addSDs [zless_eq_zadd_Suc]));
 by (simp_tac 
     (!simpset addsimps [zadd_assoc, zless_zadd_Suc, znat_add RS sym]) 1);
 qed "zless_trans";
@@ -599,9 +602,9 @@
 val zless_zsucI = zlessI RSN (2,zless_trans);
 
 goal Integ.thy "!!z w::int. z<w ==> ~w<z";
-by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc]));
+by (safe_tac (!claset addSDs [zless_eq_zadd_Suc]));
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (safe_tac intrel_cs);
+by (safe_tac (!claset));
 by (asm_full_simp_tac (!simpset addsimps ([znat_def, zadd])) 1);
 by (asm_full_simp_tac
  (!simpset delsimps [add_Suc_right] addsimps [add_left_cancel, add_assoc, add_Suc_right RS sym]) 1);
@@ -622,7 +625,7 @@
 bind_thm ("zless_irrefl", (zless_not_refl RS notE));
 
 goal Integ.thy "!!w. z<w ==> w ~= (z::int)";
-by(fast_tac (HOL_cs addEs [zless_irrefl]) 1);
+by(fast_tac (!claset addEs [zless_irrefl]) 1);
 qed "zless_not_refl2";
 
 
@@ -631,7 +634,7 @@
     "z<w | z=w | w<(z::int)";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-by (safe_tac intrel_cs);
+by (safe_tac (!claset));
 by (asm_full_simp_tac
     (!simpset addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
 by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
@@ -651,7 +654,7 @@
     "($#m < $#n) = (m<n)";
 by (simp_tac
     (!simpset addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
-by (fast_tac (HOL_cs addIs [add_commute] addSEs [less_add_eq_less]) 1);
+by (fast_tac (!claset addIs [add_commute] addSEs [less_add_eq_less]) 1);
 qed "zless_eq_less";
 
 goalw Integ.thy [zle_def, le_def] "($#m <= $#n) = (m<=n)";
@@ -669,21 +672,21 @@
 val zleE = make_elim zleD;
 
 goalw Integ.thy [zle_def] "!!z. ~ z <= w ==> w<(z::int)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "not_zleE";
 
 goalw Integ.thy [zle_def] "!!z. z < w ==> z <= (w::int)";
-by (fast_tac (HOL_cs addEs [zless_asym]) 1);
+by (fast_tac (!claset addEs [zless_asym]) 1);
 qed "zless_imp_zle";
 
 goalw Integ.thy [zle_def] "!!z. z <= w ==> z < w | z=(w::int)";
 by (cut_facts_tac [zless_linear] 1);
-by (fast_tac (HOL_cs addEs [zless_irrefl,zless_asym]) 1);
+by (fast_tac (!claset addEs [zless_irrefl,zless_asym]) 1);
 qed "zle_imp_zless_or_eq";
 
 goalw Integ.thy [zle_def] "!!z. z<w | z=w ==> z <=(w::int)";
 by (cut_facts_tac [zless_linear] 1);
-by (fast_tac (HOL_cs addEs [zless_irrefl,zless_asym]) 1);
+by (fast_tac (!claset addEs [zless_irrefl,zless_asym]) 1);
 qed "zless_or_eq_imp_zle";
 
 goal Integ.thy "(x <= (y::int)) = (x < y | x=y)";
@@ -696,17 +699,17 @@
 
 val prems = goal Integ.thy "!!i. [| i <= j; j < k |] ==> i < (k::int)";
 by (dtac zle_imp_zless_or_eq 1);
-by (fast_tac (HOL_cs addIs [zless_trans]) 1);
+by (fast_tac (!claset addIs [zless_trans]) 1);
 qed "zle_zless_trans";
 
 goal Integ.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::int)";
 by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
-            rtac zless_or_eq_imp_zle, fast_tac (HOL_cs addIs [zless_trans])]);
+            rtac zless_or_eq_imp_zle, fast_tac (!claset addIs [zless_trans])]);
 qed "zle_trans";
 
 goal Integ.thy "!!z. [| z <= w; w <= z |] ==> z = (w::int)";
 by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
-            fast_tac (HOL_cs addEs [zless_irrefl,zless_asym])]);
+            fast_tac (!claset addEs [zless_irrefl,zless_asym])]);
 qed "zle_anti_sym";
 
 
@@ -719,13 +722,13 @@
 (*** Monotonicity results ***)
 
 goal Integ.thy "!!v w z::int. v < w ==> v + z < w + z";
-by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc]));
+by (safe_tac (!claset addSDs [zless_eq_zadd_Suc]));
 by (simp_tac (!simpset addsimps zadd_ac) 1);
 by (simp_tac (!simpset addsimps [zadd_assoc RS sym, zless_zadd_Suc]) 1);
 qed "zadd_zless_mono1";
 
 goal Integ.thy "!!v w z::int. (v+z < w+z) = (v < w)";
-by (safe_tac (HOL_cs addSEs [zadd_zless_mono1]));
+by (safe_tac (!claset addSEs [zadd_zless_mono1]));
 by (dres_inst_tac [("z", "$~z")] zadd_zless_mono1 1);
 by (asm_full_simp_tac (!simpset addsimps [zadd_assoc]) 1);
 qed "zadd_left_cancel_zless";

--- a/src/HOL/Lex/Auto.ML	Mon Jul 29 18:31:39 1996 +0200
+++ b/src/HOL/Lex/Auto.ML	Tue Jul 30 17:33:26 1996 +0200
@@ -24,16 +24,16 @@
 goalw Auto.thy [acc_prefix_def]
  "acc_prefix A s (x#xs) = (fin A (next A s x) | acc_prefix A (next A s x) xs)";
 by(simp_tac (!simpset addsimps [prefix_Cons]) 1);
-by(safe_tac HOL_cs);
+by(safe_tac (!claset));
   by(Asm_full_simp_tac 1);
   by (case_tac "zs=[]" 1);
    by(hyp_subst_tac 1);
    by(Asm_full_simp_tac 1);
-  by(fast_tac (HOL_cs addSEs [Cons_neq_Nil]) 1);
+  by(fast_tac (!claset addSEs [Cons_neq_Nil]) 1);
  by(res_inst_tac [("x","[x]")] exI 1);
  by(asm_simp_tac (!simpset addsimps [eq_sym_conv]) 1);
 by(res_inst_tac [("x","x#us")] exI 1);
 by(Asm_simp_tac 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed"acc_prefix_Cons";
 Addsimps [acc_prefix_Cons];

--- a/src/HOL/Lex/AutoChopper.ML	Mon Jul 29 18:31:39 1996 +0200
+++ b/src/HOL/Lex/AutoChopper.ML	Tue Jul 30 17:33:26 1996 +0200
@@ -28,7 +28,7 @@
 by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 by (strip_tac 1);
 by (rtac conjI 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 by(simp_tac (!simpset addsimps [prefix_Cons] addcongs [conj_cong]) 1);
 by (strip_tac 1);
 by(REPEAT(eresolve_tac [conjE,exE] 1));
@@ -36,13 +36,13 @@
 by (Simp_tac 1);
 by (case_tac "zsa = []" 1);
 by (Asm_simp_tac 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 bind_thm("no_acc", result() RS spec RS spec RS mp);
 
 
 val [prem] = goal HOL.thy "? x.P(f(x)) ==> ? y.P(y)";
 by (cut_facts_tac [prem] 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 val ex_special = result();
 
 
@@ -59,7 +59,7 @@
 by (res_inst_tac[("xs","vss")] list_eq_cases 1);
  by(hyp_subst_tac 1);
  by(Simp_tac 1);
- by (fast_tac (HOL_cs addSDs [no_acc]) 1);
+ by (fast_tac (!claset addSDs [no_acc]) 1);
 by(hyp_subst_tac 1);
 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 val step2_a = (result() repeat_RS spec) RS mp;
@@ -74,7 +74,7 @@
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (list.induct_tac "xs" 1);
  by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
 by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
 by(rename_tac "vss lrst" 1);  
@@ -83,7 +83,7 @@
 by (case_tac "acc_prefix A (next A st a) list" 1);
  by(Asm_simp_tac 1);
 by (subgoal_tac "r @ [a] ~= []" 1);
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 by (Simp_tac 1);
 val step2_b = (result() repeat_RS spec) RS mp;
 
@@ -97,7 +97,7 @@
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (list.induct_tac "xs" 1);
  by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
 by (strip_tac 1);
 by (rtac conjI 1);
@@ -110,20 +110,20 @@
   by (Simp_tac 1);
   by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
    by (Simp_tac 1);
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
  by (strip_tac 1);
  by (res_inst_tac [("x","[a]")] exI 1);
  by (Asm_simp_tac 1);
  by (subgoal_tac "r @ [a] ~= []" 1);
   br sym 1;
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
  by (Simp_tac 1);
 by (strip_tac 1);
 by (res_inst_tac [("f","%k.a#k")] ex_special 1);
 by (Simp_tac 1);
 by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
  by (Simp_tac 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 val step2_c = (result() repeat_RS spec) RS mp;
 
 
@@ -136,7 +136,7 @@
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (list.induct_tac "xs" 1);
  by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
 by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
 by(rename_tac "vss lrst" 1);  
@@ -147,7 +147,7 @@
 by (subgoal_tac "acc list (start A) [] [] ([],list) A = (yss,zs)" 1);
  by (Asm_simp_tac 2);
  by (subgoal_tac "r@[a] ~= []" 2);
-  by (fast_tac HOL_cs 2);
+  by (Fast_tac 2);
  by (Simp_tac 2);
 by (subgoal_tac "flat(yss) @ zs = list" 1);
  by(hyp_subst_tac 1);
@@ -155,7 +155,7 @@
 by (case_tac "yss = []" 1);
  by (Asm_simp_tac 1);
  by (hyp_subst_tac 1);
- by (fast_tac (HOL_cs addSDs [no_acc]) 1);
+ by (fast_tac (!claset addSDs [no_acc]) 1);
 by (etac ((neq_Nil_conv RS iffD1) RS exE) 1);
 by (etac exE 1);
 by (hyp_subst_tac 1);
@@ -175,7 +175,7 @@
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (list.induct_tac "xs" 1);
  by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
 by (strip_tac 1);
 by (case_tac "acc_prefix A (next A st a) list" 1);
@@ -207,13 +207,13 @@
 by (res_inst_tac [("x","[a]")] exI 1);
 by (rtac conjI 1);
  by (subgoal_tac "r @ [a] ~= []" 1);
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
  by (Simp_tac 1);
 by (rtac list_cases 1);
  by (Simp_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [acc_prefix_def] addcongs[conj_cong]) 1);
 by (etac thin_rl 1); (* speed up *)
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 val step2_e = (result() repeat_RS spec) RS mp;
 Addsimps[split_paired_All];
 
@@ -228,7 +228,7 @@
  br mp 1;
   be step2_c 2;
  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 by (rtac conjI 1);
  by (asm_simp_tac (!simpset addsimps [step2_a] setloop (split_tac [expand_if])) 1);
 by (rtac conjI 1);
@@ -238,5 +238,5 @@
 by (rtac mp 1);
  be step2_e 2;
  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed"auto_chopper_is_auto_chopper";

--- a/src/HOL/Lex/Prefix.ML	Mon Jul 29 18:31:39 1996 +0200
+++ b/src/HOL/Lex/Prefix.ML	Tue Jul 30 17:33:26 1996 +0200
@@ -21,7 +21,7 @@
 goalw Prefix.thy [prefix_def] "(xs <= []) = (xs = [])";
 by (list.induct_tac "xs" 1);
 by (Simp_tac 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 by (Simp_tac 1);
 qed "prefix_Nil";
 Addsimps [prefix_Nil];
@@ -31,13 +31,13 @@
    "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
 by (list.induct_tac "xs" 1);
 by (Simp_tac 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 by (Simp_tac 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "prefix_Cons";
 
 goalw Prefix.thy [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)";
 by(Simp_tac 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed"Cons_prefix_Cons";
 Addsimps [Cons_prefix_Cons];