# HG changeset patch
# User berghofe
# Date 835352330 -7200
# Node ID e381e1c51689b62fe94eff4044b95cd03fa19e3c
# Parent  245721624c8dbeb06eef0c577f158ed09c4b0697
Classical tactics now use default claset.

diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/Acc.ML
--- a/src/HOL/ex/Acc.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/Acc.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -14,14 +14,14 @@
 (*The intended introduction rule*)
 val prems = goal Acc.thy
     "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)";
-by (fast_tac (set_cs addIs (prems @ 
+by (fast_tac (!claset addIs (prems @ 
                             map (rewrite_rule [pred_def]) acc.intrs)) 1);
 qed "accI";
 
 goal Acc.thy "!!a b r. [| b: acc(r);  (a,b): r |] ==> a: acc(r)";
 by (etac acc.elim 1);
 by (rewtac pred_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "acc_downward";
 
 val [major,indhyp] = goal Acc.thy
@@ -32,7 +32,7 @@
 by (rtac indhyp 1);
 by (resolve_tac acc.intrs 1);
 by (rewtac pred_def);
-by (fast_tac set_cs 2);
+by (Fast_tac 2);
 by (etac (Int_lower1 RS Pow_mono RS subsetD) 1);
 qed "acc_induct";
 
@@ -41,20 +41,20 @@
 by (rtac (major RS wfI) 1);
 by (etac acc.induct 1);
 by (rewtac pred_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "acc_wfI";
 
 val [major] = goal Acc.thy "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)";
 by (rtac (major RS wf_induct) 1);
 by (rtac (impI RS allI) 1);
 by (rtac accI 1);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "acc_wfD_lemma";
 
 val [major] = goal Acc.thy "wf(r) ==> r <= (acc r) Times (acc r)";
 by (rtac subsetI 1);
 by (res_inst_tac [("p", "x")] PairE 1);
-by (fast_tac (set_cs addSIs [SigmaI,
+by (fast_tac (!claset addSIs [SigmaI,
                              major RS acc_wfD_lemma RS spec RS mp]) 1);
 qed "acc_wfD";
 
diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/Comb.ML
--- a/src/HOL/ex/Comb.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/Comb.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -29,8 +29,8 @@
     "!!r. [| diamond(r);  (x,y):r^* |] ==> \ 
 \         ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)";
 by (etac rtrancl_induct 1);
-by (fast_tac (HOL_cs addIs [rtrancl_refl]) 1);
-by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
+by (fast_tac (!claset addIs [rtrancl_refl]) 1);
+by (slow_best_tac (!claset addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
                           addSDs [spec_mp]) 1);
 val diamond_strip_lemmaE = result() RS spec RS mp RS exE;
 
@@ -38,9 +38,9 @@
 by (rewtac diamond_def);  (*unfold only in goal, not in premise!*)
 by (rtac (impI RS allI RS allI) 1);
 by (etac rtrancl_induct 1);
-by (fast_tac (set_cs addIs [rtrancl_refl]) 1);
+by (fast_tac (!claset addIs [rtrancl_refl]) 1);
 by (ALLGOALS
-    (slow_best_tac (set_cs addIs [r_into_rtrancl, rtrancl_trans]
+    (slow_best_tac ((claset_of "Fun") addIs [r_into_rtrancl, rtrancl_trans]
                            addEs [major RS diamond_strip_lemmaE])));
 qed "diamond_rtrancl";
 
@@ -54,30 +54,29 @@
 val S_contractE = contract.mk_cases comb.simps "S -1-> z";
 val Ap_contractE = contract.mk_cases comb.simps "x#y -1-> z";
 
-val contract_cs =
-    HOL_cs addIs  contract.intrs
-	   addSEs [K_contractE, S_contractE, Ap_contractE]
-	   addss  (HOL_ss addsimps comb.simps);
+AddIs  contract.intrs;
+AddSEs [K_contractE, S_contractE, Ap_contractE];
+Addss  (HOL_ss addsimps comb.simps);
 
 goalw Comb.thy [I_def] "!!z. I -1-> z ==> P";
-by (fast_tac contract_cs 1);
+by (Fast_tac 1);
 qed "I_contract_E";
 
 (*Unused*)
 goal Comb.thy "!!x z. K#x -1-> z ==> (EX y. z = K#y & x -1-> y)";
-by (fast_tac contract_cs 1);
+by (Fast_tac 1);
 qed "K1_contractD";
 
 goal Comb.thy "!!x z. x ---> y ==> x#z ---> y#z";
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
-by (fast_tac (contract_cs addIs [r_into_rtrancl, rtrancl_trans]) 1);
+by (fast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans]) 1);
 qed "Ap_reduce1";
 
 goal Comb.thy "!!x z. x ---> y ==> z#x ---> z#y";
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
-by (fast_tac (contract_cs addIs [r_into_rtrancl, rtrancl_trans]) 1);
+by (fast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans]) 1);
 qed "Ap_reduce2";
 
 (** Counterexample to the diamond property for -1-> **)
@@ -87,15 +86,15 @@
 qed "KIII_contract1";
 
 goalw Comb.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
-by (fast_tac contract_cs 1);
+by (Fast_tac 1);
 qed "KIII_contract2";
 
 goal Comb.thy "K#I#((K#I)#(K#I)) -1-> I";
-by (fast_tac contract_cs 1);
+by (Fast_tac 1);
 qed "KIII_contract3";
 
 goalw Comb.thy [diamond_def] "~ diamond(contract)";
-by (fast_tac (HOL_cs addIs [KIII_contract1,KIII_contract2,KIII_contract3]
+by (fast_tac (!claset addIs [KIII_contract1,KIII_contract2,KIII_contract3]
                      addSEs [I_contract_E]) 1);
 qed "not_diamond_contract";
 
@@ -108,25 +107,23 @@
 val S_parcontractE = parcontract.mk_cases comb.simps "S =1=> z";
 val Ap_parcontractE = parcontract.mk_cases comb.simps "x#y =1=> z";
 
-val parcontract_cs =
-    HOL_cs addIs  parcontract.intrs
-	   addSEs [K_parcontractE, S_parcontractE, 
-		   Ap_parcontractE]
-	   addss  (HOL_ss addsimps comb.simps);
+AddIs  parcontract.intrs;
+AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE];
+Addss  (HOL_ss addsimps comb.simps);
 
 (*** Basic properties of parallel contraction ***)
 
 goal Comb.thy "!!x z. K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')";
-by (fast_tac parcontract_cs 1);
+by (Fast_tac 1);
 qed "K1_parcontractD";
 
 goal Comb.thy "!!x z. S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')";
-by (fast_tac parcontract_cs 1);
+by (Fast_tac 1);
 qed "S1_parcontractD";
 
 goal Comb.thy
  "!!x y z. S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')";
-by (fast_tac (parcontract_cs addSDs [S1_parcontractD]) 1);
+by (fast_tac (!claset addSDs [S1_parcontractD]) 1);
      (*the extra rule makes the proof more than twice as fast*)
 qed "S2_parcontractD";
 
@@ -135,7 +132,7 @@
 by (rtac (impI RS allI RS allI) 1);
 by (etac parcontract.induct 1 THEN prune_params_tac);
 by (ALLGOALS 
-    (fast_tac (parcontract_cs addSDs [K1_parcontractD,S2_parcontractD])));
+    (fast_tac (!claset addSDs [K1_parcontractD,S2_parcontractD])));
 qed "diamond_parcontract";
 
 
@@ -145,26 +142,26 @@
 by (rtac subsetI 1);
 by (split_all_tac 1);
 by (etac contract.induct 1);
-by (ALLGOALS (fast_tac (parcontract_cs)));
+by (ALLGOALS (Fast_tac));
 qed "contract_subset_parcontract";
 
 (*Reductions: simply throw together reflexivity, transitivity and
   the one-step reductions*)
-val reduce_cs = contract_cs
-                addIs [rtrancl_refl, r_into_rtrancl,
+
+AddIs [rtrancl_refl, r_into_rtrancl,
 		       contract.K, contract.S, Ap_reduce1, Ap_reduce2,
 		       rtrancl_trans];
 
 (*Example only: not used*)
 goalw Comb.thy [I_def] "I#x ---> x";
-by (best_tac reduce_cs 1);
+by (best_tac (!claset) 1);
 qed "reduce_I";
 
 goal Comb.thy "parcontract <= contract^*";
 by (rtac subsetI 1);
 by (split_all_tac 1);
 by (etac parcontract.induct 1 THEN prune_params_tac);
-by (ALLGOALS (deepen_tac reduce_cs 0));
+by (ALLGOALS (deepen_tac (!claset) 0));
 qed "parcontract_subset_reduce";
 
 goal Comb.thy "contract^* = parcontract^*";
diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/InSort.ML
--- a/src/HOL/ex/InSort.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/InSort.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -8,19 +8,19 @@
 
 goalw InSort.thy [Sorting.total_def]
   "!!f. [| total(f); ~f x y |] ==> f y x";
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
 qed "totalD";
 
 goalw InSort.thy [Sorting.transf_def]
   "!!f. [| transf(f); f b a |] ==> !x. f a x --> f b x";
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
 qed "transfD";
 
 goal InSort.thy "list_all p (ins f x xs) = (list_all p xs & p(x))";
 by(list.induct_tac "xs" 1);
 by(Asm_simp_tac 1);
 by(asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
 Addsimps [result()];
 
 goal InSort.thy "(!x. p(x) --> q(x)) --> list_all p xs --> list_all q xs";
@@ -34,7 +34,7 @@
 by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 by(cut_facts_tac prems 1);
 by(cut_inst_tac [("p","f(a)"),("q","f(x)")] list_all_imp 1);
-by(fast_tac (HOL_cs addDs [totalD,transfD]) 1);
+by(fast_tac (!claset addDs [totalD,transfD]) 1);
 Addsimps [result()];
 
 goal InSort.thy "!!f. [| total(f); transf(f) |] ==>  sorted f (insort f xs)";
diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/LList.ML
--- a/src/HOL/ex/LList.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/LList.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -27,7 +27,7 @@
 
 goal LList.thy "llist(A) = {Numb(0)} <+> (A <*> llist(A))";
 let val rew = rewrite_rule [NIL_def, CONS_def] in  
-by (fast_tac (univ_cs addSIs (equalityI :: map rew llist.intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew llist.intrs)
                       addEs [rew llist.elim]) 1)
 end;
 qed "llist_unfold";
@@ -45,12 +45,12 @@
 qed "llist_coinduct";
 
 goalw LList.thy [list_Fun_def, NIL_def] "NIL: list_Fun A X";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "list_Fun_NIL_I";
 
 goalw LList.thy [list_Fun_def,CONS_def]
     "!!M N. [| M: A;  N: X |] ==> CONS M N : list_Fun A X";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "list_Fun_CONS_I";
 
 (*Utilise the "strong" part, i.e. gfp(f)*)
@@ -99,7 +99,7 @@
     "sum_case (%u.NIL) (split(%z w. CONS z (LList_corec w f))) (f a) <= \
 \    LList_corec a f";
 by (simp_tac (!simpset addsimps [CONS_UN1]) 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
 by (ALLGOALS (res_inst_tac [("x","Suc(?k)")] UN1_I THEN' Asm_simp_tac));
 qed "LList_corec_subset2";
 
@@ -124,7 +124,7 @@
 goal LList.thy "LList_corec a f : llist({u.True})";
 by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
 by (rtac rangeI 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
 by (stac LList_corec 1);
 by (simp_tac (!simpset addsimps [list_Fun_NIL_I, list_Fun_CONS_I, CollectI]
                        |> add_eqI) 1);
@@ -136,10 +136,10 @@
 \   llist(range Leaf)";
 by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
 by (rtac rangeI 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
 by (stac LList_corec 1);
 by (asm_simp_tac (!simpset addsimps [list_Fun_NIL_I]) 1);
-by (fast_tac (set_cs addSIs [list_Fun_CONS_I]) 1);
+by (fast_tac (!claset addSIs [list_Fun_CONS_I]) 1);
 qed "LList_corec_type2";
 
 
@@ -148,16 +148,16 @@
 (*This theorem is actually used, unlike the many similar ones in ZF*)
 goal LList.thy "LListD(r) = diag({Numb(0)}) <++> (r <**> LListD(r))";
 let val rew = rewrite_rule [NIL_def, CONS_def] in  
-by (fast_tac (univ_cs addSIs (equalityI :: map rew LListD.intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew LListD.intrs)
                       addEs [rew LListD.elim]) 1)
 end;
 qed "LListD_unfold";
 
 goal LList.thy "!M N. (M,N) : LListD(diag(A)) --> ntrunc k M = ntrunc k N";
 by (res_inst_tac [("n", "k")] less_induct 1);
-by (safe_tac set_cs);
+by (safe_tac ((claset_of "Fun") delrules [equalityI]));
 by (etac LListD.elim 1);
-by (safe_tac (prod_cs addSEs [diagE]));
+by (safe_tac (((claset_of "Prod") delrules [equalityI]) addSEs [diagE]));
 by (res_inst_tac [("n", "n")] natE 1);
 by (asm_simp_tac (!simpset addsimps [ntrunc_0]) 1);
 by (rename_tac "n'" 1);
@@ -173,14 +173,14 @@
 (*avoids unfolding LListD on the rhs*)
 by (res_inst_tac [("P", "%x. fst``x <= ?B")] (LListD_unfold RS ssubst) 1);
 by (Simp_tac 1);
-by (fast_tac univ_cs 1);
+by (Fast_tac 1);
 qed "fst_image_LListD";
 
 (*This inclusion justifies the use of coinduction to show M=N*)
 goal LList.thy "LListD(diag(A)) <= diag(llist(A))";
 by (rtac subsetI 1);
 by (res_inst_tac [("p","x")] PairE 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
 by (rtac diag_eqI 1);
 by (rtac (LListD_implies_ntrunc_equality RS spec RS spec RS mp RS 
           ntrunc_equality) 1);
@@ -200,12 +200,12 @@
 qed "LListD_coinduct";
 
 goalw LList.thy [LListD_Fun_def,NIL_def] "(NIL,NIL) : LListD_Fun r s";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "LListD_Fun_NIL_I";
 
 goalw LList.thy [LListD_Fun_def,CONS_def]
  "!!x. [| x:A;  (M,N):s |] ==> (CONS x M, CONS x N) : LListD_Fun (diag A) s";
-by (fast_tac univ_cs 1);
+by (Fast_tac 1);
 qed "LListD_Fun_CONS_I";
 
 (*Utilise the "strong" part, i.e. gfp(f)*)
@@ -250,7 +250,7 @@
 by (rtac (LListD_subset_diag RS subsetD RS diagE) 1);
 by (etac LListD_coinduct 1);
 by (asm_simp_tac (!simpset addsimps [LListD_eq_diag]) 1);
-by (safe_tac prod_cs);
+by (safe_tac (!claset));
 qed "LList_equalityI";
 
 
@@ -266,7 +266,7 @@
 by (res_inst_tac [("A", "{u.True}"),
                   ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
 by (rtac rangeI 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
 by (stac prem1 1);
 by (stac prem2 1);
 by (simp_tac (!simpset addsimps [LListD_Fun_NIL_I,
@@ -324,7 +324,7 @@
   The containing set is simply the singleton {Lconst(M)}. *)
 goal LList.thy "!!M A. M:A ==> Lconst(M): llist(A)";
 by (rtac (singletonI RS llist_coinduct) 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
 by (res_inst_tac [("P", "%u. u: ?A")] (Lconst RS ssubst) 1);
 by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1));
 qed "Lconst_type";
@@ -383,27 +383,28 @@
 (** Injectiveness of CONS and LCons **)
 
 goalw LList.thy [CONS_def] "(CONS M N=CONS M' N') = (M=M' & N=N')";
-by (fast_tac (HOL_cs addSEs [Scons_inject, make_elim In1_inject]) 1);
+by (fast_tac (!claset addSEs [Scons_inject, make_elim In1_inject]) 1);
 qed "CONS_CONS_eq2";
 
 bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
 
 
 (*For reasoning about abstract llist constructors*)
-val llist_cs = set_cs addIs [Rep_llist]@llist.intrs
-                      addSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject]
-                      addSDs [inj_onto_Abs_llist RS inj_ontoD,
+
+AddIs ([Rep_llist]@llist.intrs);
+AddSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject];
+AddSDs [inj_onto_Abs_llist RS inj_ontoD,
                               inj_Rep_llist RS injD, Leaf_inject];
 
 goalw LList.thy [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)";
-by (fast_tac llist_cs 1);
+by (Fast_tac 1);
 qed "LCons_LCons_eq";
 bind_thm ("LCons_inject", (LCons_LCons_eq RS iffD1 RS conjE));
 
 val [major] = goal LList.thy "CONS M N: llist(A) ==> M: A & N: llist(A)";
 by (rtac (major RS llist.elim) 1);
 by (etac CONS_neq_NIL 1);
-by (fast_tac llist_cs 1);
+by (Fast_tac 1);
 qed "CONS_D2";
 
 
@@ -450,7 +451,7 @@
 val [major,minor] = goal LList.thy
     "[| M: llist(A);  !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)";
 by (rtac (major RS imageI RS llist_coinduct) 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
 by (etac llist.elim 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
 by (REPEAT (ares_tac [list_Fun_NIL_I, list_Fun_CONS_I, 
@@ -468,7 +469,7 @@
 val [prem] = goalw LList.thy [o_def]
     "M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)";
 by (rtac (prem RS imageI RS LList_equalityI) 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
 by (etac llist.elim 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
 by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1,
@@ -477,7 +478,7 @@
 
 val [prem] = goal LList.thy "M: llist(A) ==> Lmap (%x.x) M = M";
 by (rtac (prem RS imageI RS LList_equalityI) 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
 by (etac llist.elim 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
 by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI RS UnI1,
@@ -525,13 +526,13 @@
     "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
 by (res_inst_tac
     [("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1);
-by (fast_tac set_cs 1);
-by (safe_tac set_cs);
+by (Fast_tac 1);
+by (safe_tac (!claset));
 by (eres_inst_tac [("a", "u")] llist.elim 1);
 by (eres_inst_tac [("a", "v")] llist.elim 1);
 by (ALLGOALS
     (Asm_simp_tac THEN'
-     fast_tac (set_cs addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I])));
+     fast_tac (!claset addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I])));
 qed "Lappend_type";
 
 (*strong co-induction: bisimulation and case analysis on one variable*)
@@ -544,7 +545,7 @@
 by (eres_inst_tac [("a", "u")] llist.elim 1);
 by (asm_simp_tac (!simpset addsimps [Lappend_NIL, list_Fun_llist_I]) 1);
 by (Asm_simp_tac 1);
-by (fast_tac (set_cs addSIs [list_Fun_CONS_I]) 1);
+by (fast_tac (!claset addSIs [list_Fun_CONS_I]) 1);
 qed "Lappend_type";
 
 (**** Lazy lists as the type 'a llist -- strongly typed versions of above ****)
@@ -609,19 +610,19 @@
 \           LListD_Fun (diag A) r <= (llist A) Times (llist A)";
 by (stac llist_unfold 1);
 by (simp_tac (!simpset addsimps [NIL_def, CONS_def]) 1);
-by (fast_tac univ_cs 1);
+by (Fast_tac 1);
 qed "LListD_Fun_subset_Sigma_llist";
 
 goal LList.thy
     "prod_fun Rep_llist Rep_llist `` r <= \
 \    (llist(range Leaf)) Times (llist(range Leaf))";
-by (fast_tac (prod_cs addIs [Rep_llist]) 1);
+by (fast_tac (!claset addIs [Rep_llist]) 1);
 qed "subset_Sigma_llist";
 
 val [prem] = goal LList.thy
     "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
 \    prod_fun (Rep_llist o Abs_llist) (Rep_llist o Abs_llist) `` r <= r";
-by (safe_tac prod_cs);
+by (safe_tac (!claset));
 by (rtac (prem RS subsetD RS SigmaE2) 1);
 by (assume_tac 1);
 by (asm_simp_tac (!simpset addsimps [o_def,prod_fun,Abs_llist_inverse]) 1);
@@ -631,8 +632,8 @@
     "prod_fun Rep_llist  Rep_llist `` range(%x. (x, x)) = \
 \    diag(llist(range Leaf))";
 by (rtac equalityI 1);
-by (fast_tac (univ_cs addIs [Rep_llist]) 1);
-by (fast_tac (univ_cs addSEs [Abs_llist_inverse RS subst]) 1);
+by (fast_tac (!claset addIs [Rep_llist]) 1);
+by (fast_tac (!claset addSEs [Abs_llist_inverse RS subst]) 1);
 qed "prod_fun_range_eq_diag";
 
 (** To show two llists are equal, exhibit a bisimulation! 
@@ -736,7 +737,7 @@
 by (res_inst_tac [("r", "range(%u.(lmap f (iterates f u),iterates f (f u)))")] 
     llist_equalityI 1);
 by (rtac rangeI 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
 by (res_inst_tac [("x1", "f(u)")] (iterates RS ssubst) 1);
 by (res_inst_tac [("x1", "u")] (iterates RS ssubst) 1);
 by (simp_tac (!simpset addsimps [lmap_LCons]) 1);
@@ -776,7 +777,7 @@
 \                    nat_rec n (iterates f u) (%m y.lmap f y)))")] 
     llist_equalityI 1);
 by (REPEAT (resolve_tac [UN1_I, range_eqI, Pair_cong, nat_rec_0 RS sym] 1));
-by (safe_tac set_cs);
+by (safe_tac (!claset));
 by (stac iterates 1);
 by (stac prem 1);
 by (stac fun_power_lmap 1);
@@ -826,7 +827,7 @@
 by (res_inst_tac [("r", "range(%u.(lappend (iterates f u) N,iterates f u))")] 
     llist_equalityI 1);
 by (rtac rangeI 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
 by (stac iterates 1);
 by (simp_tac (!simpset addsimps [lappend_LCons]) 1);
 qed "lappend_iterates";
@@ -841,7 +842,7 @@
     llist_equalityI 1);
 by (rtac UN1_I 1);
 by (rtac rangeI 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
 by (res_inst_tac [("l", "l")] llistE 1);
 by (res_inst_tac [("l", "n")] llistE 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps
diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/LexProd.ML
--- a/src/HOL/ex/LexProd.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/LexProd.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -11,7 +11,7 @@
 by (cut_facts_tac prems 1);
 by (rtac allI 1);
 by (rtac (surjective_pairing RS ssubst) 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "split_all_pair";
 
 val [wfa,wfb] = goalw LexProd.thy [wf_def,LexProd.lex_prod_def]
@@ -20,5 +20,5 @@
 by (rtac (wfa RS spec RS mp) 1);
 by (EVERY1 [rtac allI,rtac impI]);
 by (rtac (wfb RS spec RS mp) 1);
-by (fast_tac (set_cs addSEs [Pair_inject]) 1);
+by (fast_tac (!claset addSEs [Pair_inject]) 1);
 qed "wf_lex_prod";
diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/MT.ML
--- a/src/HOL/ex/MT.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/MT.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -35,11 +35,11 @@
 (* ############################################################ *)
 
 val infsys_mono_tac =
-  (rewtac subset_def) THEN (safe_tac HOL_cs) THEN (rtac ballI 1) THEN
+  (rewtac subset_def) THEN (safe_tac (claset_of "HOL")) THEN (rtac ballI 1) THEN
   (rtac CollectI 1) THEN (dtac CollectD 1) THEN
   REPEAT 
     ( (TRY ((etac disjE 1) THEN (rtac disjI2 2) THEN (rtac disjI1 1))) THEN
-      (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac set_cs 1)
+      (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac ((claset_of "Fun")delrules [equalityI]) 1)
     );
 
 val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))";
@@ -102,7 +102,7 @@
 by (rtac (monoh RS monoD) 1);
 by (rtac (UnE RS subsetI) 1);
 by (assume_tac 1);
-by (fast_tac (set_cs addSIs [cih]) 1);
+by (fast_tac (!claset addSIs [cih]) 1);
 by (rtac (monoh RS monoD RS subsetD) 1);
 by (rtac Un_upper2 1);
 by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
@@ -169,7 +169,7 @@
 by (rtac lfp_intro2 1);
 by (rtac eval_fun_mono 1);
 by (rewtac eval_fun_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "eval_const";
 
 val prems = goalw MT.thy [eval_def, eval_rel_def] 
@@ -178,7 +178,7 @@
 by (rtac lfp_intro2 1);
 by (rtac eval_fun_mono 1);
 by (rewtac eval_fun_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "eval_var2";
 
 val prems = goalw MT.thy [eval_def, eval_rel_def] 
@@ -187,7 +187,7 @@
 by (rtac lfp_intro2 1);
 by (rtac eval_fun_mono 1);
 by (rewtac eval_fun_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "eval_fn";
 
 val prems = goalw MT.thy [eval_def, eval_rel_def] 
@@ -197,7 +197,7 @@
 by (rtac lfp_intro2 1);
 by (rtac eval_fun_mono 1);
 by (rewtac eval_fun_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "eval_fix";
 
 val prems = goalw MT.thy [eval_def, eval_rel_def]
@@ -207,7 +207,7 @@
 by (rtac lfp_intro2 1);
 by (rtac eval_fun_mono 1);
 by (rewtac eval_fun_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "eval_app1";
 
 val prems = goalw MT.thy [eval_def, eval_rel_def] 
@@ -220,7 +220,7 @@
 by (rtac lfp_intro2 1);
 by (rtac eval_fun_mono 1);
 by (rewtac eval_fun_def);
-by (fast_tac (set_cs addSIs [disjI2]) 1);
+by (fast_tac (!claset addSIs [disjI2]) 1);
 qed "eval_app2";
 
 (* Strong elimination, induction on evaluations *)
@@ -248,9 +248,9 @@
 by (rtac eval_fun_mono 1);
 by (rewtac eval_fun_def);
 by (dtac CollectD 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
 by (ALLGOALS (resolve_tac prems));
-by (ALLGOALS (fast_tac set_cs));
+by (ALLGOALS (Fast_tac));
 qed "eval_ind0";
 
 val prems = goal MT.thy 
@@ -293,7 +293,7 @@
 by (rtac lfp_intro2 1);
 by (rtac elab_fun_mono 1);
 by (rewtac elab_fun_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "elab_const";
 
 val prems = goalw MT.thy [elab_def, elab_rel_def] 
@@ -302,7 +302,7 @@
 by (rtac lfp_intro2 1);
 by (rtac elab_fun_mono 1);
 by (rewtac elab_fun_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "elab_var";
 
 val prems = goalw MT.thy [elab_def, elab_rel_def] 
@@ -311,7 +311,7 @@
 by (rtac lfp_intro2 1);
 by (rtac elab_fun_mono 1);
 by (rewtac elab_fun_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "elab_fn";
 
 val prems = goalw MT.thy [elab_def, elab_rel_def]
@@ -321,7 +321,7 @@
 by (rtac lfp_intro2 1);
 by (rtac elab_fun_mono 1);
 by (rewtac elab_fun_def);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "elab_fix";
 
 val prems = goalw MT.thy [elab_def, elab_rel_def] 
@@ -331,7 +331,7 @@
 by (rtac lfp_intro2 1);
 by (rtac elab_fun_mono 1);
 by (rewtac elab_fun_def);
-by (fast_tac (set_cs addSIs [disjI2]) 1);
+by (fast_tac (!claset addSIs [disjI2]) 1);
 qed "elab_app";
 
 (* Strong elimination, induction on elaborations *)
@@ -359,9 +359,9 @@
 by (rtac elab_fun_mono 1);
 by (rewtac elab_fun_def);
 by (dtac CollectD 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
 by (ALLGOALS (resolve_tac prems));
-by (ALLGOALS (fast_tac set_cs));
+by (ALLGOALS (Fast_tac));
 qed "elab_ind0";
 
 val prems = goal MT.thy
@@ -410,9 +410,9 @@
 by (rtac elab_fun_mono 1);
 by (rewtac elab_fun_def);
 by (dtac CollectD 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
 by (ALLGOALS (resolve_tac prems));
-by (ALLGOALS (fast_tac set_cs));
+by (ALLGOALS (Fast_tac));
 qed "elab_elim0";
 
 val prems = goal MT.thy
@@ -441,7 +441,7 @@
 fun elab_e_elim_tac p = 
   ( (rtac elab_elim 1) THEN 
     (resolve_tac p 1) THEN 
-    (REPEAT (fast_tac (e_ext_cs HOL_cs) 1))
+    (REPEAT (fast_tac (e_ext_cs (claset_of "HOL")) 1))
   );
 
 val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)";
@@ -451,7 +451,7 @@
 val prems = goal MT.thy "te |- e_const(c) ===> t ==> c isof t";
 by (cut_facts_tac prems 1);
 by (dtac elab_const_elim_lem 1);
-by (fast_tac prop_cs 1);
+by (Fast_tac 1);
 qed "elab_const_elim";
 
 val prems = goal MT.thy 
@@ -463,7 +463,7 @@
   "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
 by (cut_facts_tac prems 1);
 by (dtac elab_var_elim_lem 1);
-by (fast_tac prop_cs 1);
+by (Fast_tac 1);
 qed "elab_var_elim";
 
 val prems = goal MT.thy 
@@ -479,7 +479,7 @@
 \   (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
 by (cut_facts_tac prems 1);
 by (dtac elab_fn_elim_lem 1);
-by (fast_tac prop_cs 1);
+by (Fast_tac 1);
 qed "elab_fn_elim";
 
 val prems = goal MT.thy 
@@ -494,7 +494,7 @@
 \   (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
 by (cut_facts_tac prems 1);
 by (dtac elab_fix_elim_lem 1);
-by (fast_tac prop_cs 1);
+by (Fast_tac 1);
 qed "elab_fix_elim";
 
 val prems = goal MT.thy 
@@ -507,7 +507,7 @@
  "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; 
 by (cut_facts_tac prems 1);
 by (dtac elab_app_elim_lem 1);
-by (fast_tac prop_cs 1);
+by (Fast_tac 1);
 qed "elab_app_elim";
 
 (* ############################################################ *)
@@ -534,7 +534,7 @@
 by (rewtac MT.hasty_fun_def);
 by (rtac CollectI 1);
 by (rtac disjI1 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 by (rtac mono_hasty_fun 1);
 qed "hasty_rel_const_coind";
 
@@ -553,7 +553,7 @@
 by (rewtac hasty_fun_def);
 by (rtac CollectI 1);
 by (rtac disjI2 1);
-by (fast_tac HOL_cs 1);
+by (fast_tac (claset_of "HOL") 1);
 by (rtac mono_hasty_fun 1);
 qed "hasty_rel_clos_coind";
 
@@ -574,9 +574,9 @@
 by (rewtac hasty_fun_def);
 by (dtac CollectD 1);
 by (fold_goals_tac [hasty_fun_def]);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
 by (ALLGOALS (resolve_tac prems));
-by (ALLGOALS (fast_tac set_cs));
+by (ALLGOALS (Fast_tac));
 qed "hasty_rel_elim0";
 
 val prems = goal MT.thy 
@@ -605,7 +605,7 @@
   "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
 by (cut_facts_tac prems 1);
 by (rtac hasty_rel_clos_coind 1);
-by (ALLGOALS (fast_tac set_cs));
+by (ALLGOALS (Fast_tac));
 qed "hasty_clos";
 
 (* Elimination on constants for hasty *)
@@ -614,12 +614,12 @@
   "v hasty t ==> (!c.(v = v_const(c) --> c isof t))";  
 by (cut_facts_tac prems 1);
 by (rtac hasty_rel_elim 1);
-by (ALLGOALS (fast_tac (v_ext_cs HOL_cs)));
+by (ALLGOALS (fast_tac (v_ext_cs (claset_of "HOL"))));
 qed "hasty_elim_const_lem";
 
 val prems = goal MT.thy "v_const(c) hasty t ==> c isof t";
 by (cut_facts_tac (prems RL [hasty_elim_const_lem]) 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "hasty_elim_const";
 
 (* Elimination on closures for hasty *)
@@ -630,14 +630,14 @@
 \     v=v_clos(<|x,e,ve|>) --> (? te.te |- fn x => e ===> t & ve hastyenv te)";
 by (cut_facts_tac prems 1);
 by (rtac hasty_rel_elim 1);
-by (ALLGOALS (fast_tac (v_ext_cs HOL_cs)));
+by (ALLGOALS (fast_tac (v_ext_cs (claset_of "HOL"))));
 qed "hasty_elim_clos_lem";
 
 val prems = goal MT.thy 
   "v_clos(<|ev,e,ve|>) hasty t ==> ? te.te |- fn ev => e ===>\
   \t & ve hastyenv te ";
 by (cut_facts_tac (prems RL [hasty_elim_clos_lem]) 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "hasty_elim_clos";
 
 (* ############################################################ *)
@@ -650,10 +650,10 @@
 by (rewtac hasty_env_def);
 by (asm_full_simp_tac (!simpset delsimps mem_simps
                                 addsimps [ve_dom_owr, te_dom_owr]) 1);
-by (safe_tac HOL_cs);
+by (safe_tac (claset_of "HOL"));
 by (excluded_middle_tac "ev=x" 1);
 by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 by (asm_simp_tac (!simpset addsimps [ve_app_owr1, te_app_owr1]) 1);
 qed "hasty_env1";
 
@@ -673,7 +673,7 @@
 \   ve_app ve ev hasty t";
 by (cut_facts_tac prems 1);
 by (dtac elab_var_elim 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "consistency_var";
 
 val prems = goal MT.thy
@@ -681,7 +681,7 @@
 \   v_clos(<| ev, e, ve |>) hasty t";
 by (cut_facts_tac prems 1);
 by (rtac hasty_clos 1);
-by (fast_tac prop_cs 1);
+by (Fast_tac 1);
 qed "consistency_fn";
 
 val prems = goalw MT.thy [hasty_env_def,hasty_def]
@@ -692,7 +692,7 @@
 \   v_clos(cl) hasty t";
 by (cut_facts_tac prems 1);
 by (dtac elab_fix_elim 1);
-by (safe_tac HOL_cs);
+by (safe_tac (claset_of "HOL"));
 (*Do a single unfolding of cl*)
 by ((forward_tac [ssubst] 1) THEN (assume_tac 2));
 by (rtac hasty_rel_clos_coind 1);
@@ -700,16 +700,16 @@
 by (asm_simp_tac (!simpset addsimps [ve_dom_owr, te_dom_owr]) 1);
 
 by (asm_simp_tac (!simpset delsimps mem_simps addsimps [ve_dom_owr]) 1);
-by (safe_tac HOL_cs);
+by (safe_tac (claset_of "HOL"));
 by (excluded_middle_tac "ev2=ev1a" 1);
 by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 
 by (asm_simp_tac (!simpset delsimps mem_simps
                            addsimps [ve_app_owr1, te_app_owr1]) 1);
 by (hyp_subst_tac 1);
 by (etac subst 1);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "consistency_fix";
 
 val prems = goal MT.thy 
@@ -720,13 +720,13 @@
 \   v_const(c_app c1 c2) hasty t";
 by (cut_facts_tac prems 1);
 by (dtac elab_app_elim 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
 by (rtac hasty_const 1);
 by (rtac isof_app 1);
 by (rtac hasty_elim_const 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 by (rtac hasty_elim_const 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "consistency_app1";
 
 val prems = goal MT.thy 
@@ -742,7 +742,7 @@
 \   v hasty t";
 by (cut_facts_tac prems 1);
 by (dtac elab_app_elim 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
 by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
 by (assume_tac 1);
 by (etac impE 1);
@@ -752,12 +752,12 @@
 by (etac impE 1);
 by (assume_tac 1);
 by (dtac hasty_elim_clos 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
 by (dtac elab_fn_elim 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
 by (dtac t_fun_inj 1);
-by (safe_tac prop_cs);
-by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (fast_tac HOL_cs 1));
+by (safe_tac (!claset));
+by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (Fast_tac 1));
 qed "consistency_app2";
 
 val [major] = goal MT.thy 
@@ -767,7 +767,7 @@
 (* Proof by induction on the structure of evaluations *)
 
 by (rtac (major RS eval_ind) 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
 by (DEPTH_SOLVE 
     (ares_tac [consistency_const, consistency_var, consistency_fn,
                consistency_fix, consistency_app1, consistency_app2] 1));
@@ -780,7 +780,7 @@
 val prems = goalw MT.thy [isof_env_def,hasty_env_def] 
   "ve isofenv te ==> ve hastyenv te";
 by (cut_facts_tac prems 1);
-by (safe_tac HOL_cs);
+by (safe_tac (!claset));
 by (etac allE 1);
 by (etac impE 1);
 by (assume_tac 1);
@@ -795,7 +795,7 @@
 by (cut_facts_tac prems 1);
 by (rtac hasty_elim_const 1);
 by (dtac consistency 1);
-by (fast_tac (HOL_cs addSIs [basic_consistency_lem]) 1);
+by (fast_tac (!claset addSIs [basic_consistency_lem]) 1);
 qed "basic_consistency";
 
 
diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/Mutil.ML
--- a/src/HOL/ex/Mutil.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/Mutil.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -16,7 +16,7 @@
 \              u: tiling A --> t Int u = {} --> t Un u : tiling A";
 by (etac tiling.induct 1);
 by (Simp_tac 1);
-by (fast_tac (set_cs addIs tiling.intrs
+by (fast_tac (!claset addIs tiling.intrs
 	             addss (HOL_ss addsimps [Un_assoc,
 					     subset_empty_iff RS sym])) 1);
 bind_thm ("tiling_UnI", result() RS mp RS mp);
@@ -32,17 +32,17 @@
 by (res_inst_tac [("x", "i")] spec 1);
 by (nat_ind_tac "k" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [below_Suc, less_Suc_eq])));
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "below_less_iff";
 
 goal thy "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)";
 by (simp_tac (!simpset addsimps [below_Suc]) 1);
-by (fast_tac (prod_cs addIs [equalityI]) 1);
+by (fast_tac (!claset addIs [equalityI]) 1);
 qed "Sigma_Suc1";
 
 goal thy "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))";
 by (simp_tac (!simpset addsimps [below_Suc]) 1);
-by (fast_tac (prod_cs addIs [equalityI]) 1);
+by (fast_tac (!claset addIs [equalityI]) 1);
 qed "Sigma_Suc2";
 
 goal thy "{i} Times below(n + n) : tiling domino";
@@ -53,16 +53,16 @@
 by (subgoal_tac    (*seems the easiest way of turning one to the other*)
     "({i} Times {Suc(n1+n1)}) Un ({i} Times {n1+n1}) = \
 \    {(i, n1+n1), (i, Suc(n1+n1))}" 1);
-by (fast_tac (prod_cs addIs [equalityI]) 2);
+by (fast_tac (!claset addIs [equalityI]) 2);
 by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
-by (fast_tac (prod_cs addIs [equalityI, lessI] addEs [less_irrefl, less_asym]
+by (fast_tac (!claset addIs [equalityI, lessI] addEs [less_irrefl, less_asym]
                       addDs [below_less_iff RS iffD1]) 1);
 qed "dominoes_tile_row";
 
 goal thy "(below m) Times below(n + n) : tiling domino";
 by (nat_ind_tac "m" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [Sigma_Suc1])));
-by (fast_tac (prod_cs addIs [equalityI, tiling_UnI, dominoes_tile_row] 
+by (fast_tac (!claset addIs [equalityI, tiling_UnI, dominoes_tile_row] 
                       addEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
 qed "dominoes_tile_matrix";
 
@@ -81,11 +81,11 @@
 bind_thm("finite_evnodd", evnodd_subset RS finite_subset);
 
 goalw thy [evnodd_def] "evnodd (A Un B) b = evnodd A b Un evnodd B b";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "evnodd_Un";
 
 goalw thy [evnodd_def] "evnodd (A - B) b = evnodd A b - evnodd B b";
-by (fast_tac eq_cs 1);
+by (Fast_tac 1);
 qed "evnodd_Diff";
 
 goalw thy [evnodd_def] "evnodd {} b = {}";
@@ -96,7 +96,7 @@
     "evnodd (insert (i,j) C) b = \
 \    (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
 by (asm_full_simp_tac (!simpset addsimps [evnodd_def] 
-             setloop (split_tac [expand_if] THEN' step_tac eq_cs)) 1);
+             setloop (split_tac [expand_if] THEN' step_tac (!claset))) 1);
 qed "evnodd_insert";
 
 
@@ -111,11 +111,11 @@
 by (REPEAT (asm_simp_tac (!simpset addsimps
                           [evnodd_insert, evnodd_empty, mod_Suc] 
                           setloop split_tac [expand_if]) 1
-           THEN fast_tac less_cs 1));
+           THEN Fast_tac 1));
 qed "domino_singleton";
 
 goal thy "!!d. d:domino ==> finite d";
-by (fast_tac (set_cs addSIs [finite_insertI, finite_emptyI] 
+by (fast_tac (!claset addSIs [finite_insertI, finite_emptyI] 
                      addEs [domino.elim]) 1);
 qed "domino_finite";
 
@@ -125,7 +125,7 @@
 goal thy "!!t. t:tiling domino ==> finite t";
 by (eresolve_tac [tiling.induct] 1);
 by (rtac finite_emptyI 1);
-by (fast_tac (set_cs addIs [domino_finite, finite_UnI]) 1);
+by (fast_tac (!claset addIs [domino_finite, finite_UnI]) 1);
 qed "tiling_domino_finite";
 
 goal thy "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
@@ -135,13 +135,13 @@
 by (Simp_tac 2 THEN assume_tac 1);
 by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
 by (Simp_tac 2 THEN assume_tac 1);
-by (step_tac HOL_cs 1);
+by (step_tac (!claset) 1);
 by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
 by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_insert_left, 
                                      tiling_domino_finite,
                                      evnodd_subset RS finite_subset,
                                      card_insert_disjoint]) 1);
-by (fast_tac (set_cs addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
+by (fast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
 qed "tiling_domino_0_1";
 
 goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n);   \
diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/Perm.ML
--- a/src/HOL/ex/Perm.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/Perm.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -40,7 +40,7 @@
 
 goal Perm.thy "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys";
 by (etac perm.induct 1);
-by (fast_tac HOL_cs 4);
+by (Fast_tac 4);
 by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
 val perm_mem_lemma = result();
 
diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/PropLog.ML
--- a/src/HOL/ex/PropLog.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/PropLog.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -18,7 +18,7 @@
 
 (*Rule is called I for Identity Combinator, not for Introduction*)
 goal PropLog.thy "H |- p->p";
-by(best_tac (HOL_cs addIs [thms.K,thms.S,thms.MP]) 1);
+by(best_tac (!claset addIs [thms.K,thms.S,thms.MP]) 1);
 qed "thms_I";
 
 (** Weakening, left and right **)
@@ -35,14 +35,14 @@
 val weaken_left_Un2  =    Un_upper2 RS weaken_left;
 
 goal PropLog.thy "!!H. H |- q ==> H |- p->q";
-by(fast_tac (HOL_cs addIs [thms.K,thms.MP]) 1);
+by(fast_tac (!claset addIs [thms.K,thms.MP]) 1);
 qed "weaken_right";
 
 (*The deduction theorem*)
 goal PropLog.thy "!!H. insert p H |- q  ==>  H |- p->q";
 by (etac thms.induct 1);
 by (ALLGOALS 
-    (fast_tac (set_cs addIs [thms_I, thms.H, thms.K, thms.S, thms.DN, 
+    (fast_tac (!claset addIs [thms_I, thms.H, thms.K, thms.S, thms.DN, 
 			     thms.S RS thms.MP RS thms.MP, weaken_right])));
 qed "deduction";
 
@@ -77,7 +77,7 @@
 (*Soundness of the rules wrt truth-table semantics*)
 goalw PropLog.thy [sat_def] "!!H. H |- p ==> H |= p";
 by (etac thms.induct 1);
-by (fast_tac (set_cs addSDs [eval_imp RS iffD1 RS mp]) 5);
+by (fast_tac (!claset addSDs [eval_imp RS iffD1 RS mp]) 5);
 by (ALLGOALS Asm_simp_tac);
 qed "soundness";
 
@@ -104,7 +104,7 @@
 by (rtac (expand_if RS iffD2) 1);
 by(PropLog.pl.induct_tac "p" 1);
 by (ALLGOALS (simp_tac (!simpset addsimps [thms_I, thms.H])));
-by (fast_tac (set_cs addIs [weaken_left_Un1, weaken_left_Un2, 
+by (fast_tac (!claset addIs [weaken_left_Un1, weaken_left_Un2, 
                            weaken_right, imp_false]
                     addSEs [false_imp]) 1);
 qed "hyps_thms_if";
@@ -113,18 +113,19 @@
 val [sat] = goalw PropLog.thy [sat_def] "{} |= p ==> hyps p tt |- p";
 by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN
     rtac hyps_thms_if 2);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "sat_thms_p";
 
 (*For proving certain theorems in our new propositional logic*)
-val thms_cs = 
-    set_cs addSIs [deduction] addIs [thms.H, thms.H RS thms.MP];
+
+AddSIs [deduction];
+AddIs [thms.H, thms.H RS thms.MP];
 
 (*The excluded middle in the form of an elimination rule*)
 goal PropLog.thy "H |- (p->q) -> ((p->false)->q) -> q";
 by (rtac (deduction RS deduction) 1);
 by (rtac (thms.DN RS thms.MP) 1);
-by (ALLGOALS (best_tac (thms_cs addSIs prems)));
+by (ALLGOALS (best_tac (!claset addSIs prems)));
 qed "thms_excluded_middle";
 
 (*Hard to prove directly because it requires cuts*)
@@ -143,7 +144,7 @@
 by (Simp_tac 1);
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (Simp_tac 1);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "hyps_Diff";
 
 (*For the case hyps(p,t)-insert(#v -> false,Y) |- p;
@@ -153,17 +154,17 @@
 by (Simp_tac 1);
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (Simp_tac 1);
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "hyps_insert";
 
 (** Two lemmas for use with weaken_left **)
 
 goal Set.thy "B-C <= insert a (B-insert a C)";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "insert_Diff_same";
 
 goal Set.thy "insert a (B-{c}) - D <= insert a (B-insert c D)";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "insert_Diff_subset2";
 
 (*The set hyps(p,t) is finite, and elements have the form #v or #v->false;
@@ -171,7 +172,7 @@
 goal PropLog.thy "hyps p t : Fin(UN v:{x.True}. {#v, #v->false})";
 by (PropLog.pl.induct_tac "p" 1);
 by (ALLGOALS (simp_tac (!simpset setloop (split_tac [expand_if]))));
-by (ALLGOALS (fast_tac (set_cs addSIs Fin.intrs@[Fin_UnI])));
+by (ALLGOALS (fast_tac (!claset addSIs Fin.intrs@[Fin_UnI])));
 qed "hyps_finite";
 
 val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
@@ -182,7 +183,7 @@
     "{} |= p ==> !t. hyps p t - hyps p t0 |- p";
 by (rtac (hyps_finite RS Fin_induct) 1);
 by (simp_tac (!simpset addsimps [sat RS sat_thms_p]) 1);
-by (safe_tac set_cs);
+by (safe_tac (!claset));
 (*Case hyps(p,t)-insert(#v,Y) |- p *)
 by (rtac thms_excluded_middle_rule 1);
 by (rtac (insert_Diff_same RS weaken_left) 1);
@@ -213,16 +214,16 @@
 
 val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> !p. H |= p --> H |- p";
 by (rtac (finite RS Fin_induct) 1);
-by (safe_tac (set_cs addSIs [completeness_0]));
+by (safe_tac ((claset_of "Fun") addSIs [completeness_0]));
 by (rtac (weaken_left_insert RS thms.MP) 1);
-by (fast_tac (set_cs addSIs [sat_imp]) 1);
-by (fast_tac thms_cs 1);
+by (fast_tac ((claset_of "Fun") addSIs [sat_imp]) 1);
+by (Fast_tac 1);
 qed "completeness_lemma";
 
 val completeness = completeness_lemma RS spec RS mp;
 
 val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> (H |- p) = (H |= p)";
-by (fast_tac (set_cs addSEs [soundness, finite RS completeness]) 1);
+by (fast_tac (!claset addSEs [soundness, finite RS completeness]) 1);
 qed "thms_iff";
 
 writeln"Reached end of file.";
diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/Puzzle.ML
--- a/src/HOL/ex/Puzzle.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/Puzzle.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -21,38 +21,38 @@
 by (rtac classical 1);
 by (dtac not_leE 1);
 by (subgoal_tac "f(na) <= f(f(na))" 1);
-by (best_tac (HOL_cs addIs [lessD,Puzzle.f_ax,le_less_trans,le_trans]) 1);
-by (fast_tac (HOL_cs addIs [Puzzle.f_ax]) 1);
+by (best_tac (!claset addIs [lessD,Puzzle.f_ax,le_less_trans,le_trans]) 1);
+by (fast_tac (!claset addIs [Puzzle.f_ax]) 1);
 val lemma = result() RS spec RS mp;
 
 goal Puzzle.thy "n <= f(n)";
-by (fast_tac (HOL_cs addIs [lemma]) 1);
+by (fast_tac (!claset addIs [lemma]) 1);
 qed "lemma1";
 
 goal Puzzle.thy "f(n) < f(Suc(n))";
-by (fast_tac (HOL_cs addIs [Puzzle.f_ax,le_less_trans,lemma1]) 1);
+by (fast_tac (!claset addIs [Puzzle.f_ax,le_less_trans,lemma1]) 1);
 qed "lemma2";
 
 val prems = goal Puzzle.thy "(!!n.f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)";
 by (res_inst_tac[("n","n")]nat_induct 1);
 by (Simp_tac 1);
 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
-by (fast_tac (HOL_cs addIs (le_trans::prems)) 1);
+by (fast_tac (!claset addIs (le_trans::prems)) 1);
 bind_thm("mono_lemma1", result() RS mp);
 
 val [p1,p2] = goal Puzzle.thy
     "[| !! n. f(n)<=f(Suc(n));  m<=n |] ==> f(m) <= f(n)";
 by (rtac (p2 RS le_imp_less_or_eq RS disjE) 1);
 by (etac (p1 RS mono_lemma1) 1);
-by (fast_tac (HOL_cs addIs [le_refl]) 1);
+by (fast_tac (!claset addIs [le_refl]) 1);
 qed "mono_lemma";
 
 val prems = goal Puzzle.thy "m <= n ==> f(m) <= f(n)";
-by (fast_tac (HOL_cs addIs ([mono_lemma,less_imp_le,lemma2]@prems)) 1);
+by (fast_tac (!claset addIs ([mono_lemma,less_imp_le,lemma2]@prems)) 1);
 qed "f_mono";
 
 goal Puzzle.thy "f(n) = n";
 by (rtac le_anti_sym 1);
 by (rtac lemma1 2);
-by (fast_tac (HOL_cs addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,lessD]) 1);
+by (fast_tac (!claset addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,lessD]) 1);
 result();
diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/Qsort.ML
--- a/src/HOL/ex/Qsort.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/Qsort.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -27,7 +27,7 @@
 Addsimps [alls_lemma];
 
 goal HOL.thy "((P --> Q) & (~P --> Q)) = Q";
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
 val lemma = result();
 
 goal Qsort.thy "(Alls x:qsort le xs.P(x))  =  (Alls x:xs.P(x))";
@@ -55,7 +55,7 @@
 by(asm_full_simp_tac (!simpset addsimps []) 1);
 by(asm_full_simp_tac (!simpset addsimps [list_all_mem_conv]) 1);
 by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
 result();
 
 (* A verification based on predicate calculus rather than combinators *)
@@ -69,7 +69,7 @@
 goal Qsort.thy "x mem qsort le xs = x mem xs";
 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
 by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
 Addsimps [result()];
 
 goal Qsort.thy
@@ -80,7 +80,7 @@
 by(asm_simp_tac (!simpset setloop (split_tac [expand_if])
 			  delsimps [list_all_conj]
 			  addsimps [list_all_mem_conv]) 1);
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
 Addsimps [result()];
 
 goal Qsort.thy
@@ -91,7 +91,7 @@
 			  delsimps [list_all_conj]
 			  addsimps [list_all_mem_conv]) 1);
 by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
 result();
 
 
diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/SList.ML
--- a/src/HOL/ex/SList.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/SList.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -12,7 +12,7 @@
 
 goal SList.thy "list(A) = {Numb(0)} <+> (A <*> list(A))";
 let val rew = rewrite_rule list_con_defs in  
-by (fast_tac (univ_cs addSIs (equalityI :: map rew list.intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew list.intrs)
                       addEs [rew list.elim]) 1)
 end;
 qed "list_unfold";
@@ -26,7 +26,7 @@
 (*Type checking -- list creates well-founded sets*)
 goalw SList.thy (list_con_defs @ list.defs) "list(sexp) <= sexp";
 by (rtac lfp_lowerbound 1);
-by (fast_tac (univ_cs addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1);
+by (fast_tac (!claset addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1);
 qed "list_sexp";
 
 (* A <= sexp ==> list(A) <= sexp *)
@@ -82,32 +82,32 @@
 (** Injectiveness of CONS and Cons **)
 
 goalw SList.thy [CONS_def] "(CONS K M=CONS L N) = (K=L & M=N)";
-by (fast_tac (HOL_cs addSEs [Scons_inject, make_elim In1_inject]) 1);
+by (fast_tac (!claset addSEs [Scons_inject, make_elim In1_inject]) 1);
 qed "CONS_CONS_eq";
 
 bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
 
 (*For reasoning about abstract list constructors*)
-val list_cs = set_cs addIs [Rep_list] @ list.intrs
-                     addSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject]
-                     addSDs [inj_onto_Abs_list RS inj_ontoD,
-                             inj_Rep_list RS injD, Leaf_inject];
+AddIs ([Rep_list] @ list.intrs);
+AddSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject];
+AddSDs [inj_onto_Abs_list RS inj_ontoD,
+        inj_Rep_list RS injD, Leaf_inject];
 
 goalw SList.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)";
-by (fast_tac list_cs 1);
+by (Fast_tac 1);
 qed "Cons_Cons_eq";
 bind_thm ("Cons_inject2", (Cons_Cons_eq RS iffD1 RS conjE));
 
 val [major] = goal SList.thy "CONS M N: list(A) ==> M: A & N: list(A)";
 by (rtac (major RS setup_induction) 1);
 by (etac list.induct 1);
-by (ALLGOALS (fast_tac list_cs));
+by (ALLGOALS (Fast_tac));
 qed "CONS_D";
 
 val prems = goalw SList.thy [CONS_def,In1_def]
     "CONS M N: sexp ==> M: sexp & N: sexp";
 by (cut_facts_tac prems 1);
-by (fast_tac (set_cs addSDs [Scons_D]) 1);
+by (fast_tac (!claset addSDs [Scons_D]) 1);
 qed "sexp_CONS_D";
 
 
@@ -343,7 +343,7 @@
 \                        (!y ys. xs=y#ys --> P(f y ys)))";
 by(list_ind_tac "xs" 1);
 by(ALLGOALS Asm_simp_tac);
-by(fast_tac HOL_cs 1);
+by(Fast_tac 1);
 qed "expand_list_case2";
 
 
diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/Simult.ML
--- a/src/HOL/ex/Simult.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/Simult.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -29,7 +29,7 @@
 
 goalw Simult.thy [TF_def] "TF(sexp) <= sexp";
 by (rtac lfp_lowerbound 1);
-by (fast_tac (univ_cs addIs  sexp.intrs@[sexp_In0I, sexp_In1I]
+by (fast_tac (!claset addIs  sexp.intrs@[sexp_In0I, sexp_In1I]
                       addSEs [PartE]) 1);
 qed "TF_sexp";
 
@@ -50,7 +50,7 @@
 \            |] ==> R(FCONS M N)    \
 \    |] ==> R(i)";
 by (rtac ([TF_def, TF_fun_mono, major] MRS def_induct) 1);
-by (fast_tac (set_cs addIs (prems@[PartI])
+by (fast_tac (!claset addIs (prems@[PartI])
                        addEs [usumE, uprodE, PartE]) 1);
 qed "TF_induct";
 
@@ -61,9 +61,9 @@
 by (cfast_tac prems 1);
 qed "TF_induct_lemma";
 
-val uplus_cs = set_cs addSIs [PartI]
-                      addSDs [In0_inject, In1_inject]
-                      addSEs [In0_neq_In1, In1_neq_In0, PartE];
+AddSIs [PartI];
+AddSDs [In0_inject, In1_inject];
+AddSEs [In0_neq_In1, In1_neq_In0, PartE];
 
 (*Could prove  ~ TCONS M N : Part (TF A) In1  etc. *)
 
@@ -77,7 +77,7 @@
 by (rtac (ballI RS TF_induct_lemma) 1);
 by (etac TF_induct 1);
 by (rewrite_goals_tac TF_Rep_defs);
-by (ALLGOALS (fast_tac (uplus_cs addIs prems)));
+by (ALLGOALS (fast_tac (!claset addIs prems)));
 (*29 secs??*)
 qed "Tree_Forest_induct";
 
@@ -91,11 +91,11 @@
                   ("Q1","%z.Q(Abs_Forest(z))")] 
     (Tree_Forest_induct RS conjE) 1);
 (*Instantiates ?A1 to range(Leaf). *)
-by (fast_tac (set_cs addSEs [Rep_Tree_inverse RS subst, 
+by (fast_tac (!claset addSEs [Rep_Tree_inverse RS subst, 
                              Rep_Forest_inverse RS subst] 
                      addSIs [Rep_Tree,Rep_Forest]) 4);
 (*Cannot use simplifier: the rewrites work in the wrong direction!*)
-by (ALLGOALS (fast_tac (set_cs addSEs [Abs_Tree_inverse RS subst,
+by (ALLGOALS (fast_tac (!claset addSEs [Abs_Tree_inverse RS subst,
                           Abs_Forest_inverse RS subst] 
                      addSIs prems)));
 qed "tree_forest_induct";
@@ -131,41 +131,41 @@
 val TF_I = TF_unfold RS equalityD2 RS subsetD;
 
 (*For reasoning about the representation*)
-val TF_Rep_cs = uplus_cs addIs [TF_I, uprodI, usum_In0I, usum_In1I]
-                         addSEs [Scons_inject];
+AddIs [TF_I, uprodI, usum_In0I, usum_In1I];
+AddSEs [Scons_inject];
 
 val prems = goalw Simult.thy TF_Rep_defs
     "[| a: A;  M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
-by (fast_tac (TF_Rep_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
 qed "TCONS_I";
 
 (* FNIL is a TF(A) -- this also justifies the type definition*)
 goalw Simult.thy TF_Rep_defs "FNIL: Part (TF A) In1";
-by (fast_tac TF_Rep_cs 1);
+by (Fast_tac 1);
 qed "FNIL_I";
 
 val prems = goalw Simult.thy TF_Rep_defs
     "[| M: Part (TF A) In0;  N: Part (TF A) In1 |] ==> \
 \    FCONS M N : Part (TF A) In1";
-by (fast_tac (TF_Rep_cs addIs prems) 1);
+by (fast_tac (!claset addIs prems) 1);
 qed "FCONS_I";
 
 (** Injectiveness of TCONS and FCONS **)
 
 goalw Simult.thy TF_Rep_defs "(TCONS K M=TCONS L N) = (K=L & M=N)";
-by (fast_tac TF_Rep_cs 1);
+by (Fast_tac 1);
 qed "TCONS_TCONS_eq";
 bind_thm ("TCONS_inject", (TCONS_TCONS_eq RS iffD1 RS conjE));
 
 goalw Simult.thy TF_Rep_defs "(FCONS K M=FCONS L N) = (K=L & M=N)";
-by (fast_tac TF_Rep_cs 1);
+by (Fast_tac 1);
 qed "FCONS_FCONS_eq";
 bind_thm ("FCONS_inject", (FCONS_FCONS_eq RS iffD1 RS conjE));
 
 (** Distinctness of TCONS, FNIL and FCONS **)
 
 goalw Simult.thy TF_Rep_defs "TCONS M N ~= FNIL";
-by (fast_tac TF_Rep_cs 1);
+by (Fast_tac 1);
 qed "TCONS_not_FNIL";
 bind_thm ("FNIL_not_TCONS", (TCONS_not_FNIL RS not_sym));
 
@@ -173,7 +173,7 @@
 val FNIL_neq_TCONS = sym RS TCONS_neq_FNIL;
 
 goalw Simult.thy TF_Rep_defs "FCONS M N ~= FNIL";
-by (fast_tac TF_Rep_cs 1);
+by (Fast_tac 1);
 qed "FCONS_not_FNIL";
 bind_thm ("FNIL_not_FCONS", (FCONS_not_FNIL RS not_sym));
 
@@ -181,7 +181,7 @@
 val FNIL_neq_FCONS = sym RS FCONS_neq_FNIL;
 
 goalw Simult.thy TF_Rep_defs "TCONS M N ~= FCONS K L";
-by (fast_tac TF_Rep_cs 1);
+by (Fast_tac 1);
 qed "TCONS_not_FCONS";
 bind_thm ("FCONS_not_TCONS", (TCONS_not_FCONS RS not_sym));
 
@@ -194,23 +194,23 @@
 (** Injectiveness of Tcons and Fcons **)
 
 (*For reasoning about abstract constructors*)
-val TF_cs = set_cs addSIs [Rep_Tree, Rep_Forest, TCONS_I, FNIL_I, FCONS_I]
-                   addSEs [TCONS_inject, FCONS_inject,
+AddSIs [Rep_Tree, Rep_Forest, TCONS_I, FNIL_I, FCONS_I];
+AddSEs [TCONS_inject, FCONS_inject,
                            TCONS_neq_FNIL, FNIL_neq_TCONS,
                            FCONS_neq_FNIL, FNIL_neq_FCONS,
-                           TCONS_neq_FCONS, FCONS_neq_TCONS]
-                   addSDs [inj_onto_Abs_Tree RS inj_ontoD,
+                           TCONS_neq_FCONS, FCONS_neq_TCONS];
+AddSDs [inj_onto_Abs_Tree RS inj_ontoD,
                            inj_onto_Abs_Forest RS inj_ontoD,
                            inj_Rep_Tree RS injD, inj_Rep_Forest RS injD,
                            Leaf_inject];
 
 goalw Simult.thy [Tcons_def] "(Tcons x xs=Tcons y ys) = (x=y & xs=ys)";
-by (fast_tac TF_cs 1);
+by (Fast_tac 1);
 qed "Tcons_Tcons_eq";
 bind_thm ("Tcons_inject", (Tcons_Tcons_eq RS iffD1 RS conjE));
 
 goalw Simult.thy [Fcons_def,Fnil_def] "Fcons x xs ~= Fnil";
-by (fast_tac TF_cs 1);
+by (Fast_tac 1);
 qed "Fcons_not_Fnil";
 
 bind_thm ("Fcons_neq_Fnil", Fcons_not_Fnil RS notE);
@@ -220,7 +220,7 @@
 (** Injectiveness of Fcons **)
 
 goalw Simult.thy [Fcons_def] "(Fcons x xs=Fcons y ys) = (x=y & xs=ys)";
-by (fast_tac TF_cs 1);
+by (Fast_tac 1);
 qed "Fcons_Fcons_eq";
 bind_thm ("Fcons_inject", Fcons_Fcons_eq RS iffD1 RS conjE);
 
diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/Term.ML
--- a/src/HOL/ex/Term.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/Term.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -12,7 +12,7 @@
 (*** Monotonicity and unfolding of the function ***)
 
 goal Term.thy "term(A) = A <*> list(term(A))";
-by (fast_tac (univ_cs addSIs (equalityI :: term.intrs)
+by (fast_tac (!claset addSIs (equalityI :: term.intrs)
                       addEs [term.elim]) 1);
 qed "term_unfold";
 
@@ -25,7 +25,7 @@
 
 goalw Term.thy term.defs "term(sexp) <= sexp";
 by (rtac lfp_lowerbound 1);
-by (fast_tac (univ_cs addIs [sexp.SconsI, list_sexp RS subsetD]) 1);
+by (fast_tac (!claset addIs [sexp.SconsI, list_sexp RS subsetD]) 1);
 qed "term_sexp";
 
 (* A <= sexp ==> term(A) <= sexp *)
diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/cla.ML
--- a/src/HOL/ex/cla.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/cla.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -11,17 +11,17 @@
 writeln"File HOL/ex/cla.";
 
 goal HOL.thy "(P --> Q | R) --> (P-->Q) | (P-->R)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 (*If and only if*)
 
 goal HOL.thy "(P=Q) = (Q=P::bool)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 goal HOL.thy "~ (P = (~P))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 
@@ -38,112 +38,112 @@
 writeln"Pelletier's examples";
 (*1*)
 goal HOL.thy "(P-->Q)  =  (~Q --> ~P)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 (*2*)
 goal HOL.thy "(~ ~ P) =  P";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 (*3*)
 goal HOL.thy "~(P-->Q) --> (Q-->P)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 (*4*)
 goal HOL.thy "(~P-->Q)  =  (~Q --> P)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 (*5*)
 goal HOL.thy "((P|Q)-->(P|R)) --> (P|(Q-->R))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 (*6*)
 goal HOL.thy "P | ~ P";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 (*7*)
 goal HOL.thy "P | ~ ~ ~ P";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 (*8.  Peirce's law*)
 goal HOL.thy "((P-->Q) --> P)  -->  P";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 (*9*)
 goal HOL.thy "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 (*10*)
 goal HOL.thy "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
 goal HOL.thy "P=P::bool";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 (*12.  "Dijkstra's law"*)
 goal HOL.thy "((P = Q) = R) = (P = (Q = R))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 (*13.  Distributive law*)
 goal HOL.thy "(P | (Q & R)) = ((P | Q) & (P | R))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 (*14*)
 goal HOL.thy "(P = Q) = ((Q | ~P) & (~Q|P))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 (*15*)
 goal HOL.thy "(P --> Q) = (~P | Q)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 (*16*)
 goal HOL.thy "(P-->Q) | (Q-->P)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 (*17*)
 goal HOL.thy "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 writeln"Classical Logic: examples with quantifiers";
 
 goal HOL.thy "(! x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result(); 
 
 goal HOL.thy "(? x. P-->Q(x))  =  (P --> (? x.Q(x)))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result(); 
 
 goal HOL.thy "(? x.P(x)-->Q) = ((! x.P(x)) --> Q)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result(); 
 
 goal HOL.thy "((! x.P(x)) | Q)  =  (! x. P(x) | Q)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result(); 
 
 (*From Wishnu Prasetya*)
 goal HOL.thy
    "(!s. q(s) --> r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) --> p(t) | q(t)) \
 \   --> p(t) | r(t)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result(); 
 
 
@@ -151,60 +151,60 @@
 
 (*Needs multiple instantiation of the quantifier.*)
 goal HOL.thy "(! x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
 result();
 
 (*Needs double instantiation of the quantifier*)
 goal HOL.thy "? x. P(x) --> P(a) & P(b)";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
 result();
 
 goal HOL.thy "? z. P(z) --> (! x. P(x))";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
 result();
 
 goal HOL.thy "? x. (? y. P(y)) --> P(x)";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
 result();
 
 writeln"Hard examples with quantifiers";
 
 writeln"Problem 18";
 goal HOL.thy "? y. ! x. P(y)-->P(x)";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
 result(); 
 
 writeln"Problem 19";
 goal HOL.thy "? x. ! y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
 result();
 
 writeln"Problem 20";
 goal HOL.thy "(! x y. ? z. ! w. (P(x)&Q(y)-->R(z)&S(w)))     \
 \   --> (? x y. P(x) & Q(y)) --> (? z. R(z))";
-by (fast_tac HOL_cs 1); 
+by (Fast_tac 1); 
 result();
 
 writeln"Problem 21";
 goal HOL.thy "(? x. P-->Q(x)) & (? x. Q(x)-->P) --> (? x. P=Q(x))";
-by (deepen_tac HOL_cs 1 1); 
+by (deepen_tac (!claset) 1 1); 
 result();
 
 writeln"Problem 22";
 goal HOL.thy "(! x. P = Q(x))  -->  (P = (! x. Q(x)))";
-by (fast_tac HOL_cs 1); 
+by (Fast_tac 1); 
 result();
 
 writeln"Problem 23";
 goal HOL.thy "(! x. P | Q(x))  =  (P | (! x. Q(x)))";
-by (best_tac HOL_cs 1);  
+by (best_tac (!claset) 1);  
 result();
 
 writeln"Problem 24";
 goal HOL.thy "~(? x. S(x)&Q(x)) & (! x. P(x) --> Q(x)|R(x)) &  \
 \    ~(? x.P(x)) --> (? x.Q(x)) & (! x. Q(x)|R(x) --> S(x))  \
 \   --> (? x. P(x)&R(x))";
-by (fast_tac HOL_cs 1); 
+by (Fast_tac 1); 
 result();
 
 writeln"Problem 25";
@@ -213,14 +213,14 @@
 \       (! x. P(x) --> (M(x) & L(x))) &   \
 \       ((! x. P(x)-->Q(x)) | (? x. P(x)&R(x)))  \
 \   --> (? x. Q(x)&P(x))";
-by (best_tac HOL_cs 1); 
+by (best_tac (!claset) 1); 
 result();
 
 writeln"Problem 26";
 goal HOL.thy "((? x. p(x)) = (? x. q(x))) &     \
 \     (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \
 \ --> ((! x. p(x)-->r(x)) = (! x. q(x)-->s(x)))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 writeln"Problem 27";
@@ -229,7 +229,7 @@
 \             (! x. M(x) & L(x) --> P(x)) &   \
 \             ((? x. R(x) & ~ Q(x)) --> (! x. L(x) --> ~ R(x)))  \
 \         --> (! x. M(x) --> ~L(x))";
-by (fast_tac HOL_cs 1); 
+by (Fast_tac 1); 
 result();
 
 writeln"Problem 28.  AMENDED";
@@ -237,21 +237,21 @@
 \       ((! x. Q(x)|R(x)) --> (? x. Q(x)&S(x))) &  \
 \       ((? x.S(x)) --> (! x. L(x) --> M(x)))  \
 \   --> (! x. P(x) & L(x) --> M(x))";
-by (fast_tac HOL_cs 1);  
+by (Fast_tac 1);  
 result();
 
 writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
 goal HOL.thy "(? x. F(x)) & (? y. G(y))  \
 \   --> ( ((! x. F(x)-->H(x)) & (! y. G(y)-->J(y)))  =   \
 \         (! x y. F(x) & G(y) --> H(x) & J(y)))";
-by (fast_tac HOL_cs 1); 
+by (Fast_tac 1); 
 result();
 
 writeln"Problem 30";
 goal HOL.thy "(! x. P(x) | Q(x) --> ~ R(x)) & \
 \       (! x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
 \   --> (! x. S(x))";
-by (fast_tac HOL_cs 1);  
+by (Fast_tac 1);  
 result();
 
 writeln"Problem 31";
@@ -259,7 +259,7 @@
 \       (? x. L(x) & P(x)) & \
 \       (! x. ~ R(x) --> M(x))  \
 \   --> (? x. L(x) & M(x))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 writeln"Problem 32";
@@ -267,13 +267,13 @@
 \       (! x. S(x) & R(x) --> L(x)) & \
 \       (! x. M(x) --> R(x))  \
 \   --> (! x. P(x) & M(x) --> L(x))";
-by (best_tac HOL_cs 1);
+by (best_tac (!claset) 1);
 result();
 
 writeln"Problem 33";
 goal HOL.thy "(! x. P(a) & (P(x)-->P(b))-->P(c))  =    \
 \    (! x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
-by (best_tac HOL_cs 1);
+by (best_tac (!claset) 1);
 result();
 
 writeln"Problem 34  AMENDED (TWICE!!)";
@@ -282,13 +282,13 @@
 \                   ((? x. q(x)) = (! y. p(y))))   =    \
 \                  ((? x. ! y. q(x) = q(y))  =          \
 \                   ((? x. p(x)) = (! y. q(y))))";
-by (deepen_tac HOL_cs 3 1);
+by (deepen_tac (!claset) 3 1);
 (*slower with smaller bounds*)
 result();
 
 writeln"Problem 35";
 goal HOL.thy "? x y. P x y -->  (! u v. P u v)";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
 result();
 
 writeln"Problem 36";
@@ -297,7 +297,7 @@
 \       (! x y. J x y | G x y -->       \
 \       (! z. J y z | G y z --> H x z))   \
 \   --> (! x. ? y. H x y)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 writeln"Problem 37";
@@ -306,7 +306,7 @@
 \       (! x z. ~(P x z) --> (? y. Q y z)) & \
 \       ((? x y. Q x y) --> (! x. R x x))  \
 \   --> (! x. ? y. R x y)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 writeln"Problem 38";
@@ -316,29 +316,29 @@
 \    (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) &  \
 \          (~p(a) | ~(? y. p(y) & r x y) |                      \
 \           (? z. ? w. p(z) & r x w & r w z)))";
-by (deepen_tac HOL_cs 0 1);  (*beats fast_tac!*)
+by (deepen_tac (!claset) 0 1);  (*beats fast_tac!*)
 result();
 
 writeln"Problem 39";
 goal HOL.thy "~ (? x. ! y. F y x = (~ F y y))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 writeln"Problem 40.  AMENDED";
 goal HOL.thy "(? y. ! x. F x y = F x x)  \
 \       -->  ~ (! x. ? y. ! z. F z y = (~ F z x))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 writeln"Problem 41";
 goal HOL.thy "(! z. ? y. ! x. f x y = (f x z & ~ f x x))        \
 \              --> ~ (? z. ! x. f x z)";
-by (best_tac HOL_cs 1);
+by (best_tac (!claset) 1);
 result();
 
 writeln"Problem 42";
 goal HOL.thy "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))";
-by (deepen_tac HOL_cs 3 1);
+by (deepen_tac (!claset) 3 1);
 result();
 
 writeln"Problem 43  NOT PROVED AUTOMATICALLY";
@@ -352,7 +352,7 @@
 \             (? y. g(y) & h x y & (? y. g(y) & ~ h x y)))  &   \
 \             (? x. j(x) & (! y. g(y) --> h x y))               \
 \             --> (? x. j(x) & ~f(x))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 writeln"Problem 45";
@@ -363,7 +363,7 @@
 \    (? x. f(x) & (! y. h x y --> l(y))                         \
 \               & (! y. g(y) & h x y --> j x y))                \
 \     --> (? x. f(x) & ~ (? y. g(y) & h x y))";
-by (best_tac HOL_cs 1); 
+by (best_tac (!claset) 1); 
 result();
 
 
@@ -371,7 +371,7 @@
 
 writeln"Problem 48";
 goal HOL.thy "(a=b | c=d) & (a=c | b=d) --> a=d | b=c";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 writeln"Problem 49  NOT PROVED AUTOMATICALLY";
@@ -379,25 +379,25 @@
   the type constraint ensures that x,y,z have the same type as a,b,u. *)
 goal HOL.thy "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \
 \               --> (! u::'a.P(u))";
-by (Classical.safe_tac HOL_cs);
+by (Classical.safe_tac (!claset));
 by (res_inst_tac [("x","a")] allE 1);
 by (assume_tac 1);
 by (res_inst_tac [("x","b")] allE 1);
 by (assume_tac 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 writeln"Problem 50";  
 (*What has this to do with equality?*)
 goal HOL.thy "(! x. P a x | (! y.P x y)) --> (? x. ! y.P x y)";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
 result();
 
 writeln"Problem 51";
 goal HOL.thy
     "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
 \    (? z. ! x. ? w. (! y. P x y = (y=w)) = (x=z))";
-by (best_tac HOL_cs 1);
+by (best_tac (!claset) 1);
 result();
 
 writeln"Problem 52";
@@ -405,7 +405,7 @@
 goal HOL.thy
     "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
 \    (? w. ! y. ? z. (! x. P x y = (x=z)) = (y=w))";
-by (best_tac HOL_cs 1);
+by (best_tac (!claset) 1);
 result();
 
 writeln"Problem 55";
@@ -421,37 +421,37 @@
 \  (!x. hates agatha x --> hates butler x) & \
 \  (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \
 \   killed ?who agatha";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 writeln"Problem 56";
 goal HOL.thy
     "(! x. (? y. P(y) & x=f(y)) --> P(x)) = (! x. P(x) --> P(f(x)))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 writeln"Problem 57";
 goal HOL.thy
     "P (f a b) (f b c) & P (f b c) (f a c) & \
 \    (! x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 writeln"Problem 58  NOT PROVED AUTOMATICALLY";
 goal HOL.thy "(! x y. f(x)=g(y)) --> (! x y. f(f(x))=f(g(y)))";
 val f_cong = read_instantiate [("f","f")] arg_cong;
-by (fast_tac (HOL_cs addIs [f_cong]) 1);
+by (fast_tac (!claset addIs [f_cong]) 1);
 result();
 
 writeln"Problem 59";
 goal HOL.thy "(! x. P(x) = (~P(f(x)))) --> (? x. P(x) & ~P(f(x)))";
-by (deepen_tac HOL_cs 1 1);
+by (deepen_tac (!claset) 1 1);
 result();
 
 writeln"Problem 60";
 goal HOL.thy
     "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 writeln"Problem 62 as corrected in AAR newletter #31";
@@ -459,7 +459,7 @@
     "(ALL x. p a & (p x --> p(f x)) --> p(f(f x)))  =   \
 \    (ALL x. (~ p a | p x | p(f(f x))) &                        \
 \            (~ p a | ~ p(f x) | p(f(f x))))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 (*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.  
@@ -468,14 +468,14 @@
     "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) &        \
 \    (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y)))  &        \
 \    (ALL x. K(x) --> ~G(x))   -->   (EX x. K(x) --> ~G(x))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 goal Prod.thy
     "(ALL x y. R(x,y) | R(y,x)) &                \
 \    (ALL x y. S(x,y) & S(y,x) --> x=y) &        \
 \    (ALL x y. R(x,y) --> S(x,y))    -->   (ALL x y. S(x,y) --> R(x,y))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 result();
 
 
diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/meson.ML
--- a/src/HOL/ex/meson.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/meson.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -16,7 +16,7 @@
 (*Prove theorems using fast_tac*)
 fun prove_fun s = 
     prove_goal HOL.thy s
-         (fn prems => [ cut_facts_tac prems 1, fast_tac HOL_cs 1 ]);
+         (fn prems => [ cut_facts_tac prems 1, Fast_tac 1 ]);
 
 (**** Negation Normal Form ****)
 
@@ -63,7 +63,7 @@
 val [major] = goal HOL.thy
     "! x. ? y. Q x y ==> ? f. ! x. Q x (f x)";
 by (cut_facts_tac [major] 1);
-by (fast_tac (HOL_cs addEs [selectI]) 1);
+by (fast_tac (!claset addEs [selectI]) 1);
 qed "choice";
 
 
@@ -430,7 +430,7 @@
 
 (*First, breaks the goal into independent units*)
 val safe_best_meson_tac =
-     SELECT_GOAL (TRY (safe_tac HOL_cs) THEN 
+     SELECT_GOAL (TRY (safe_tac (!claset)) THEN 
                   TRYALL (best_meson_tac size_of_subgoals));
 
 (** Depth-first search version **)
@@ -464,7 +464,7 @@
 	                   (prolog_step_tac' (make_horns cls))));
 
 val safe_meson_tac =
-     SELECT_GOAL (TRY (safe_tac HOL_cs) THEN 
+     SELECT_GOAL (TRY (safe_tac (!claset)) THEN 
                   TRYALL (iter_deepen_meson_tac));
 
 
diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/rel.ML
--- a/src/HOL/ex/rel.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/rel.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -34,7 +34,7 @@
 (*** domain ***)
 
 val [prem] = goalw Rel.thy [domain_def,Pair_def] "(a,b): r ==> a : domain(r)";
-by (fast_tac (set_cs addIs [prem]) 1);
+by (fast_tac (!claset addIs [prem]) 1);
 qed "domainI";
 
 val major::prems = goalw Rel.thy [domain_def]
@@ -48,7 +48,7 @@
 (*** range2 ***)
 
 val [prem] = goalw Rel.thy [range2_def,Pair_def] "(a,b): r ==> b : range2(r)";
-by (fast_tac (set_cs addIs [prem]) 1);
+by (fast_tac (!claset addIs [prem]) 1);
 qed "range2I";
 
 val major::prems = goalw Rel.thy [range2_def]
@@ -102,8 +102,8 @@
 \    ==>  wf(r)";
 by (rtac (prem1 RS wfI) 1);
 by (res_inst_tac [ ("B", "A-Z") ] (prem2 RS subsetCE) 1);
-by (fast_tac ZF_cs 3);
-by (fast_tac ZF_cs 2);
-by (fast_tac ZF_cs 1);
+by (Fast_tac 3);
+by (Fast_tac 2);
+by (Fast_tac 1);
 qed "wfI2";
 
diff -r 245721624c8d -r e381e1c51689 src/HOL/ex/set.ML
--- a/src/HOL/ex/set.ML	Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/set.ML	Fri Jun 21 12:18:50 1996 +0200
@@ -20,12 +20,12 @@
 
 goal Set.thy "~ (? f:: 'a=>'a set. ! S. ? x. f(x) = S)";
 (*requires best-first search because it is undirectional*)
-by (best_tac (set_cs addSEs [equalityCE]) 1);
+by (best_tac (!claset addSEs [equalityCE]) 1);
 qed "cantor1";
 
 (*This form displays the diagonal term*)
 goal Set.thy "! f:: 'a=>'a set. ! x. f(x) ~= ?S(f)";
-by (best_tac (set_cs addSEs [equalityCE]) 1);
+by (best_tac (!claset addSEs [equalityCE]) 1);
 uresult();
 
 (*This form exploits the set constructs*)
@@ -39,15 +39,15 @@
 by (assume_tac 1);
 
 choplev 0;
-by (best_tac (set_cs addSEs [equalityCE]) 1);
+by (best_tac (!claset addSEs [equalityCE]) 1);
 
 (*** The Schroder-Berstein Theorem ***)
 
 val prems = goalw Lfp.thy [image_def] "inj(f) ==> Inv(f)``(f``X) = X";
 by (cut_facts_tac prems 1);
 by (rtac equalityI 1);
-by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1);
-by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1);
+by (fast_tac (!claset addEs [Inv_f_f RS ssubst]) 1);
+by (fast_tac (!claset addEs [Inv_f_f RS ssubst]) 1);
 qed "inv_image_comp";
 
 val prems = goal Set.thy "f(a) ~: (f``X) ==> a~:X";
@@ -55,7 +55,7 @@
 qed "contra_imageI";
 
 goal Lfp.thy "(a ~: Compl(X)) = (a:X)";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "not_Compl";
 
 (*Lots of backtracking in this proof...*)
@@ -69,22 +69,22 @@
 goal Lfp.thy "range(%z. if z:X then f(z) else g(z)) = f``X Un g``Compl(X)";
 by (rtac equalityI 1);
 by (rewtac range_def);
-by (fast_tac (set_cs addIs [if_P RS sym, if_not_P RS sym]) 2);
+by (fast_tac (!claset addIs [if_P RS sym, if_not_P RS sym]) 2);
 by (rtac subsetI 1);
 by (etac CollectE 1);
 by (etac exE 1);
 by (etac ssubst 1);
 by (rtac (excluded_middle RS disjE) 1);
-by (EVERY' [rtac (if_P     RS ssubst), atac, fast_tac set_cs] 2);
-by (EVERY' [rtac (if_not_P RS ssubst), atac, fast_tac set_cs] 1);
+by (EVERY' [rtac (if_P     RS ssubst), atac, Fast_tac] 2);
+by (EVERY' [rtac (if_not_P RS ssubst), atac, Fast_tac] 1);
 qed "range_if_then_else";
 
 goal Lfp.thy "a : X Un Compl(X)";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "X_Un_Compl";
 
 goalw Lfp.thy [surj_def] "surj(f) = (!a. a : range(f))";
-by (fast_tac (set_cs addEs [ssubst]) 1);
+by (fast_tac (!claset addEs [ssubst]) 1);
 qed "surj_iff_full_range";
 
 val [compl] = goal Lfp.thy
@@ -105,9 +105,9 @@
 by (rewtac inj_def);
 by (cut_facts_tac [injf,injg] 1);
 by (EVERY1 [rtac allI, rtac allI, stac expand_if, rtac conjI, stac expand_if]);
-by (fast_tac (set_cs addEs  [inj_ontoD, sym RS f_eq_gE]) 1);
+by (fast_tac (!claset addEs  [inj_ontoD, sym RS f_eq_gE]) 1);
 by (stac expand_if 1);
-by (fast_tac (set_cs addEs  [inj_ontoD, f_eq_gE]) 1);
+by (fast_tac (!claset addEs  [inj_ontoD, f_eq_gE]) 1);
 qed "bij_if_then_else";
 
 goal Lfp.thy "? X. X = Compl(g``Compl((f:: 'a=>'b)``X))";