# HG changeset patch
# User berghofe
# Date 838981526 -7200
# Node ID 0075a8d26a8016dd04c6b60028dd1362cedf60f7
# Parent  260a9711f5078fc85193e700772a3d389950d5ec
Classical tactics now use default claset.

diff -r 260a9711f507 -r 0075a8d26a80 src/HOL/AxClasses/Group/GroupDefs.ML
--- a/src/HOL/AxClasses/Group/GroupDefs.ML	Fri Aug 02 12:16:11 1996 +0200
+++ b/src/HOL/AxClasses/Group/GroupDefs.ML	Fri Aug 02 12:25:26 1996 +0200
@@ -7,23 +7,23 @@
 (*this is really overkill - should be rather proven 'inline'*)
 
 goalw thy [times_bool_def] "(x * y) * z = x * (y * (z::bool))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "bool_assoc";
 
 goalw thy [times_bool_def, one_bool_def] "1 * x = (x::bool)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "bool_left_unit";
 
 goalw thy [times_bool_def, one_bool_def] "x * 1 = (x::bool)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "bool_right_unit";
 
 goalw thy [times_bool_def, inv_bool_def, one_bool_def] "inv(x) * x = (1::bool)";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "bool_left_inv";
 
 goalw thy [times_bool_def] "x * y = (y * (x::bool))";
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "bool_commut";
 
 
diff -r 260a9711f507 -r 0075a8d26a80 src/HOL/AxClasses/Lattice/CLattice.ML
--- a/src/HOL/AxClasses/Lattice/CLattice.ML	Fri Aug 02 12:16:11 1996 +0200
+++ b/src/HOL/AxClasses/Lattice/CLattice.ML	Fri Aug 02 12:25:26 1996 +0200
@@ -19,9 +19,9 @@
 qed "Inf_uniq";
 
 goalw thy [Ex1_def] "ALL A. EX! inf::'a::clattice. is_Inf A inf";
-  by (safe_tac HOL_cs);
-  by (step_tac HOL_cs 1);
-  by (step_tac HOL_cs 1);
+  by (safe_tac (!claset));
+  by (Step_tac 1);
+  by (Step_tac 1);
   br Inf_is_Inf 1;
   br (Inf_uniq RS mp RS sym) 1;
   ba 1;
@@ -41,9 +41,9 @@
 qed "Sup_uniq";
 
 goalw thy [Ex1_def] "ALL A. EX! sup::'a::clattice. is_Sup A sup";
-  by (safe_tac HOL_cs);
-  by (step_tac HOL_cs 1);
-  by (step_tac HOL_cs 1);
+  by (safe_tac (!claset));
+  by (Step_tac 1);
+  by (Step_tac 1);
   br Sup_is_Sup 1;
   br (Sup_uniq RS mp RS sym) 1;
   ba 1;
@@ -57,15 +57,15 @@
   br selectI2 1;
   br Inf_is_Inf 1;
   by (rewtac is_Inf_def);
-  by (fast_tac set_cs 1);
+  by (Fast_tac 1);
 qed "Inf_lb";
 
 val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A";
   br selectI2 1;
   br Inf_is_Inf 1;
   by (rewtac is_Inf_def);
-  by (step_tac HOL_cs 1);
-  by (step_tac HOL_cs 1);
+  by (Step_tac 1);
+  by (Step_tac 1);
   be mp 1;
   br ballI 1;
   be prem 1;
@@ -77,15 +77,15 @@
   br selectI2 1;
   br Sup_is_Sup 1;
   by (rewtac is_Sup_def);
-  by (fast_tac set_cs 1);
+  by (Fast_tac 1);
 qed "Sup_ub";
 
 val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z";
   br selectI2 1;
   br Sup_is_Sup 1;
   by (rewtac is_Sup_def);
-  by (step_tac HOL_cs 1);
-  by (step_tac HOL_cs 1);
+  by (Step_tac 1);
+  by (Step_tac 1);
   be mp 1;
   br ballI 1;
   be prem 1;
@@ -103,7 +103,7 @@
     be Inf_lb 1;
   (*<==*)
     br Inf_ub_lbs 1;
-    by (fast_tac set_cs 1);
+    by (Fast_tac 1);
 qed "le_Inf_eq";
 
 goal thy "(Sup A [= x) = (ALL y:A. y [= x)";
@@ -116,7 +116,7 @@
     ba 1;
   (*<==*)
     br Sup_lb_ubs 1;
-    by (fast_tac set_cs 1);
+    by (Fast_tac 1);
 qed "ge_Sup_eq";
 
 
@@ -127,7 +127,7 @@
   br impI 1;
   by (stac le_Inf_eq 1);
   by (rewtac Ball_def);
-  by (safe_tac set_cs);
+  by (safe_tac (!claset));
   bd subsetD 1;
   ba 1;
   be Inf_lb 1;
@@ -137,7 +137,7 @@
   br impI 1;
   by (stac ge_Sup_eq 1);
   by (rewtac Ball_def);
-  by (safe_tac set_cs);
+  by (safe_tac (!claset));
   bd subsetD 1;
   ba 1;
   be Sup_ub 1;
@@ -149,35 +149,35 @@
 goal thy "Inf {x} = x";
   br (Inf_uniq RS mp) 1;
   by (rewtac is_Inf_def);
-  by (safe_tac set_cs);
+  by (safe_tac (!claset));
   br le_refl 1;
-  by (fast_tac set_cs 1);
+  by (Fast_tac 1);
 qed "sing_Inf_eq";
 
 goal thy "Sup {x} = x";
   br (Sup_uniq RS mp) 1;
   by (rewtac is_Sup_def);
-  by (safe_tac set_cs);
+  by (safe_tac (!claset));
   br le_refl 1;
-  by (fast_tac set_cs 1);
+  by (Fast_tac 1);
 qed "sing_Sup_eq";
 
 
 goal thy "Inf {} = Sup {x. True}";
   br (Inf_uniq RS mp) 1;
   by (rewtac is_Inf_def);
-  by (safe_tac set_cs);
+  by (safe_tac (!claset));
   br (sing_Sup_eq RS subst) 1;
   back();
   br (Sup_subset_mon RS mp) 1;
-  by (fast_tac set_cs 1);
+  by (Fast_tac 1);
 qed "empty_Inf_eq";
 
 goal thy "Sup {} = Inf {x. True}";
   br (Sup_uniq RS mp) 1;
   by (rewtac is_Sup_def);
-  by (safe_tac set_cs);
+  by (safe_tac (!claset));
   br (sing_Inf_eq RS subst) 1;
   br (Inf_subset_antimon RS mp) 1;
-  by (fast_tac set_cs 1);
+  by (Fast_tac 1);
 qed "empty_Sup_eq";
diff -r 260a9711f507 -r 0075a8d26a80 src/HOL/AxClasses/Lattice/LatInsts.ML
--- a/src/HOL/AxClasses/Lattice/LatInsts.ML	Fri Aug 02 12:16:11 1996 +0200
+++ b/src/HOL/AxClasses/Lattice/LatInsts.ML	Fri Aug 02 12:25:26 1996 +0200
@@ -21,7 +21,7 @@
 goal thy "Inf (A Un B) = Inf A && Inf B";
   br (Inf_uniq RS mp) 1;
   by (rewtac is_Inf_def);
-  by (safe_tac set_cs);
+  by (safe_tac (!claset));
 
   br (conjI RS (le_trans RS mp)) 1;
   br inf_lb1 1;
@@ -34,26 +34,26 @@
   by (stac le_inf_eq 1);
   br conjI 1;
   br Inf_ub_lbs 1;
-  by (fast_tac set_cs 1);
+  by (Fast_tac 1);
   br Inf_ub_lbs 1;
-  by (fast_tac set_cs 1);
+  by (Fast_tac 1);
 qed "Inf_Un_eq";
 
 goal thy "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}";
   br (Inf_uniq RS mp) 1;
   by (rewtac is_Inf_def);
-  by (safe_tac set_cs);
+  by (safe_tac (!claset));
   (*level 3*)
   br (conjI RS (le_trans RS mp)) 1;
   be Inf_lb 2;
   br (sing_Inf_eq RS subst) 1;
   br (Inf_subset_antimon RS mp) 1;
-  by (fast_tac set_cs 1);
+  by (Fast_tac 1);
   (*level 8*)
   by (stac le_Inf_eq 1);
-  by (safe_tac set_cs);
+  by (safe_tac (!claset));
   by (stac le_Inf_eq 1);
-  by (fast_tac set_cs 1);
+  by (Fast_tac 1);
 qed "Inf_UN_eq";
 
 
@@ -61,7 +61,7 @@
 goal thy "Sup (A Un B) = Sup A || Sup B";
   br (Sup_uniq RS mp) 1;
   by (rewtac is_Sup_def);
-  by (safe_tac set_cs);
+  by (safe_tac (!claset));
 
   br (conjI RS (le_trans RS mp)) 1;
   be Sup_ub 1;
@@ -74,25 +74,25 @@
   by (stac ge_sup_eq 1);
   br conjI 1;
   br Sup_lb_ubs 1;
-  by (fast_tac set_cs 1);
+  by (Fast_tac 1);
   br Sup_lb_ubs 1;
-  by (fast_tac set_cs 1);
+  by (Fast_tac 1);
 qed "Sup_Un_eq";
 
 goal thy "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}";
   br (Sup_uniq RS mp) 1;
   by (rewtac is_Sup_def);
-  by (safe_tac set_cs);
+  by (safe_tac (!claset));
   (*level 3*)
   br (conjI RS (le_trans RS mp)) 1;
   be Sup_ub 1;
   br (sing_Sup_eq RS subst) 1;
   back();
   br (Sup_subset_mon RS mp) 1;
-  by (fast_tac set_cs 1);
+  by (Fast_tac 1);
   (*level 8*)
   by (stac ge_Sup_eq 1);
-  by (safe_tac set_cs);
+  by (safe_tac (!claset));
   by (stac ge_Sup_eq 1);
-  by (fast_tac set_cs 1);
+  by (Fast_tac 1);
 qed "Sup_UN_eq";
diff -r 260a9711f507 -r 0075a8d26a80 src/HOL/AxClasses/Lattice/LatMorph.ML
--- a/src/HOL/AxClasses/Lattice/LatMorph.ML	Fri Aug 02 12:16:11 1996 +0200
+++ b/src/HOL/AxClasses/Lattice/LatMorph.ML	Fri Aug 02 12:25:26 1996 +0200
@@ -5,16 +5,16 @@
 (** monotone functions vs. "&&"- / "||"-semi-morphisms **)
 
 goalw thy [is_mono_def] "is_mono f = (ALL x y. f (x && y) [= f x && f y)";
-  by (safe_tac set_cs);
+  by (safe_tac (!claset));
   (*==> (level 1)*)
     by (stac le_inf_eq 1);
     br conjI 1;
-    by (step_tac set_cs 1);
-    by (step_tac set_cs 1);
+    by (Step_tac 1);
+    by (Step_tac 1);
     be mp 1;
     br inf_lb1 1;
-    by (step_tac set_cs 1);
-    by (step_tac set_cs 1);
+    by (Step_tac 1);
+    by (Step_tac 1);
     be mp 1;
     br inf_lb2 1;
   (*==> (level 11)*)
@@ -22,22 +22,22 @@
     br inf_lb2 2;
     by (subgoal_tac "x && y = x" 1);
     be subst 1;
-    by (fast_tac set_cs 1);
+    by (Fast_tac 1);
     by (stac inf_connect 1);
     ba 1;
 qed "mono_inf_eq";
 
 goalw thy [is_mono_def] "is_mono f = (ALL x y. f x || f y [= f (x || y))";
-  by (safe_tac set_cs);
+  by (safe_tac (!claset));
   (*==> (level 1)*)
     by (stac ge_sup_eq 1);
     br conjI 1;
-    by (step_tac set_cs 1);
-    by (step_tac set_cs 1);
+    by (Step_tac 1);
+    by (Step_tac 1);
     be mp 1;
     br sup_ub1 1;
-    by (step_tac set_cs 1);
-    by (step_tac set_cs 1);
+    by (Step_tac 1);
+    by (Step_tac 1);
     be mp 1;
     br sup_ub2 1;
   (*==> (level 11)*)
@@ -45,7 +45,7 @@
     br sup_ub1 1;
     by (subgoal_tac "x || y = y" 1);
     be subst 1;
-    by (fast_tac set_cs 1);
+    by (Fast_tac 1);
     by (stac sup_connect 1);
     ba 1;
 qed "mono_sup_eq";
diff -r 260a9711f507 -r 0075a8d26a80 src/HOL/AxClasses/Lattice/LatPreInsts.ML
--- a/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Fri Aug 02 12:16:11 1996 +0200
+++ b/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Fri Aug 02 12:25:26 1996 +0200
@@ -22,13 +22,13 @@
 
 goalw thy [is_inf_def, le_prod_def] "is_inf p q (fst p && fst q, snd p && snd q)";
   by (Simp_tac 1);
-  by (safe_tac HOL_cs);
+  by (safe_tac (!claset));
   by (REPEAT_FIRST (fn i => resolve_tac [inf_lb1, inf_lb2, inf_ub_lbs] i ORELSE atac i));
 qed "prod_is_inf";
 
 goalw thy [is_sup_def, le_prod_def] "is_sup p q (fst p || fst q, snd p || snd q)";
   by (Simp_tac 1);
-  by (safe_tac HOL_cs);
+  by (safe_tac (!claset));
   by (REPEAT_FIRST (fn i => resolve_tac [sup_ub1, sup_ub2, sup_lb_ubs] i ORELSE atac i));
 qed "prod_is_sup";
 
@@ -36,19 +36,19 @@
 (* functions *)
 
 goalw thy [is_inf_def, le_fun_def] "is_inf f g (%x. f x && g x)";
-  by (safe_tac HOL_cs);
+  by (safe_tac (!claset));
   br inf_lb1 1;
   br inf_lb2 1;
   br inf_ub_lbs 1;
-  by (REPEAT_FIRST (fast_tac HOL_cs));
+  by (REPEAT_FIRST (Fast_tac));
 qed "fun_is_inf";
 
 goalw thy [is_sup_def, le_fun_def] "is_sup f g (%x. f x || g x)";
-  by (safe_tac HOL_cs);
+  by (safe_tac (!claset));
   br sup_ub1 1;
   br sup_ub2 1;
   br sup_lb_ubs 1;
-  by (REPEAT_FIRST (fast_tac HOL_cs));
+  by (REPEAT_FIRST (Fast_tac));
 qed "fun_is_sup";
 
 
@@ -57,7 +57,7 @@
 
 goalw thy [is_inf_def, le_dual_def] "is_inf x y (Abs_dual (Rep_dual x || Rep_dual y))";
   by (stac Abs_dual_inverse' 1);
-  by (safe_tac HOL_cs);
+  by (safe_tac (!claset));
   br sup_ub1 1;
   br sup_ub2 1;
   br sup_lb_ubs 1;
@@ -67,7 +67,7 @@
 
 goalw thy [is_sup_def, le_dual_def] "is_sup x y (Abs_dual (Rep_dual x && Rep_dual y))";
   by (stac Abs_dual_inverse' 1);
-  by (safe_tac HOL_cs);
+  by (safe_tac (!claset));
   br inf_lb1 1;
   br inf_lb2 1;
   br inf_ub_lbs 1;
diff -r 260a9711f507 -r 0075a8d26a80 src/HOL/AxClasses/Lattice/Lattice.ML
--- a/src/HOL/AxClasses/Lattice/Lattice.ML	Fri Aug 02 12:16:11 1996 +0200
+++ b/src/HOL/AxClasses/Lattice/Lattice.ML	Fri Aug 02 12:25:26 1996 +0200
@@ -19,9 +19,9 @@
 qed "inf_uniq";
 
 goalw thy [Ex1_def] "ALL x y. EX! inf::'a::lattice. is_inf x y inf";
-  by (safe_tac HOL_cs);
-  by (step_tac HOL_cs 1);
-  by (step_tac HOL_cs 1);
+  by (safe_tac (!claset));
+  by (Step_tac 1);
+  by (Step_tac 1);
   br inf_is_inf 1;
   br (inf_uniq RS mp RS sym) 1;
   ba 1;
@@ -41,9 +41,9 @@
 qed "sup_uniq";
 
 goalw thy [Ex1_def] "ALL x y. EX! sup::'a::lattice. is_sup x y sup";
-  by (safe_tac HOL_cs);
-  by (step_tac HOL_cs 1);
-  by (step_tac HOL_cs 1);
+  by (safe_tac (!claset));
+  by (Step_tac 1);
+  by (Step_tac 1);
   br sup_is_sup 1;
   br (sup_uniq RS mp RS sym) 1;
   ba 1;
@@ -55,7 +55,7 @@
 val tac =
   cut_facts_tac [inf_is_inf] 1 THEN
   rewrite_goals_tac [inf_def, is_inf_def] THEN
-  fast_tac HOL_cs 1;
+  Fast_tac 1;
 
 goal thy "x && y [= x";
   by tac;
@@ -74,7 +74,7 @@
 val tac =
   cut_facts_tac [sup_is_sup] 1 THEN
   rewrite_goals_tac [sup_def, is_sup_def] THEN
-  fast_tac HOL_cs 1;
+  Fast_tac 1;
 
 goal thy "x [= x || y";
   by tac;
@@ -106,7 +106,7 @@
     by (REPEAT_FIRST (rtac conjI));
     br le_refl 1;
     ba 1;
-    by (fast_tac HOL_cs 1);
+    by (Fast_tac 1);
 qed "inf_connect";
 
 goal thy "(x || y = y) = (x [= y)";
@@ -120,7 +120,7 @@
     by (REPEAT_FIRST (rtac conjI));
     ba 1;
     br le_refl 1;
-    by (fast_tac HOL_cs 1);
+    by (Fast_tac 1);
 qed "sup_connect";
 
 
diff -r 260a9711f507 -r 0075a8d26a80 src/HOL/AxClasses/Lattice/OrdDefs.ML
--- a/src/HOL/AxClasses/Lattice/OrdDefs.ML	Fri Aug 02 12:16:11 1996 +0200
+++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML	Fri Aug 02 12:25:26 1996 +0200
@@ -13,7 +13,7 @@
 qed "le_prod_refl";
 
 goalw thy [le_prod_def] "x [= y & y [= z --> x [= (z::'a::quasi_order*'b::quasi_order)";
-  by (safe_tac HOL_cs);
+  by (safe_tac (!claset));
   be (conjI RS (le_trans RS mp)) 1;
   ba 1;
   be (conjI RS (le_trans RS mp)) 1;
@@ -21,7 +21,7 @@
 qed "le_prod_trans";
 
 goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::order*'b::order)";
-  by (safe_tac HOL_cs);
+  by (safe_tac (!claset));
   by (stac Pair_fst_snd_eq 1);
   br conjI 1;
   be (conjI RS (le_antisym RS mp)) 1;
@@ -39,16 +39,16 @@
 qed "le_fun_refl";
 
 goalw thy [le_fun_def] "f [= g & g [= h --> f [= (h::'a=>'b::quasi_order)";
-  by (safe_tac HOL_cs);
+  by (safe_tac (!claset));
   br (le_trans RS mp) 1;
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
 qed "le_fun_trans";
 
 goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::order)";
-  by (safe_tac HOL_cs);
+  by (safe_tac (!claset));
   br ext 1;
   br (le_antisym RS mp) 1;
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
 qed "le_fun_antisym";
 
 
@@ -59,7 +59,7 @@
 goal thy "Rep_dual (Abs_dual y) = y";
   br Abs_dual_inverse 1;
   by (rewtac dual_def);
-  by (fast_tac set_cs 1);
+  by (Fast_tac 1);
 qed "Abs_dual_inverse'";
 
 
@@ -73,7 +73,7 @@
 qed "le_dual_trans";
 
 goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::order dual)";
-  by (safe_tac prop_cs);
+  by (safe_tac (!claset));
   br (Rep_dual_inverse RS subst) 1;
   br sym 1;
   br (Rep_dual_inverse RS subst) 1;
diff -r 260a9711f507 -r 0075a8d26a80 src/HOL/AxClasses/Lattice/Order.ML
--- a/src/HOL/AxClasses/Lattice/Order.ML	Fri Aug 02 12:16:11 1996 +0200
+++ b/src/HOL/AxClasses/Lattice/Order.ML	Fri Aug 02 12:25:26 1996 +0200
@@ -9,7 +9,7 @@
 val tac =
   rtac impI 1 THEN
   rtac (le_antisym RS mp) 1 THEN
-  fast_tac HOL_cs 1;
+  Fast_tac 1;
 
 
 goalw thy [is_inf_def] "is_inf x y inf & is_inf x y inf' --> inf = inf'";
@@ -34,24 +34,24 @@
 (* commutativity *)
 
 goalw thy [is_inf_def] "is_inf x y inf = is_inf y x inf";
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
 qed "is_inf_commut";
 
 goalw thy [is_sup_def] "is_sup x y sup = is_sup y x sup";
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
 qed "is_sup_commut";
 
 
 (* associativity *)
 
 goalw thy [is_inf_def] "is_inf x y xy & is_inf y z yz & is_inf xy z xyz --> is_inf x yz xyz";
-  by (safe_tac HOL_cs);
+  by (safe_tac (!claset));
   (*level 1*)
     br (le_trans RS mp) 1;
     be conjI 1;
     ba 1;
   (*level 4*)
-    by (step_tac HOL_cs 1);
+    by (Step_tac 1);
     back();
     be mp 1;
     br conjI 1;
@@ -60,12 +60,12 @@
     ba 1;
     ba 1;
   (*level 11*)
-    by (step_tac HOL_cs 1);
+    by (Step_tac 1);
     back();
     back();
     be mp 1;
     br conjI 1;
-    by (step_tac HOL_cs 1);
+    by (Step_tac 1);
     be mp 1;
     be conjI 1;
     br (le_trans RS mp) 1;
@@ -79,13 +79,13 @@
 
 
 goalw thy [is_sup_def] "is_sup x y xy & is_sup y z yz & is_sup xy z xyz --> is_sup x yz xyz";
-  by (safe_tac HOL_cs);
+  by (safe_tac (!claset));
   (*level 1*)
     br (le_trans RS mp) 1;
     be conjI 1;
     ba 1;
   (*level 4*)
-    by (step_tac HOL_cs 1);
+    by (Step_tac 1);
     back();
     be mp 1;
     br conjI 1;
@@ -94,12 +94,12 @@
     ba 1;
     ba 1;
   (*level 11*)
-    by (step_tac HOL_cs 1);
+    by (Step_tac 1);
     back();
     back();
     be mp 1;
     br conjI 1;
-    by (step_tac HOL_cs 1);
+    by (Step_tac 1);
     be mp 1;
     be conjI 1;
     br (le_trans RS mp) 1;
@@ -120,14 +120,14 @@
   (*case "x [= y"*)
     br le_refl 1;
     ba 1;
-    by (fast_tac HOL_cs 1);
+    by (Fast_tac 1);
   (*case "~ x [= y"*)
     br (le_lin RS disjE) 1;
     ba 1;
     be notE 1;
     ba 1;
     br le_refl 1;
-    by (fast_tac HOL_cs 1);
+    by (Fast_tac 1);
 qed "min_is_inf";
 
 goalw thy [maximum_def, is_sup_def] "is_sup (x::'a::lin_order) y (maximum x y)";
@@ -136,14 +136,14 @@
   (*case "x [= y"*)
     ba 1;
     br le_refl 1;
-    by (fast_tac HOL_cs 1);
+    by (Fast_tac 1);
   (*case "~ x [= y"*)
     br le_refl 1;
     br (le_lin RS disjE) 1;
     ba 1;
     be notE 1;
     ba 1;
-    by (fast_tac HOL_cs 1);
+    by (Fast_tac 1);
 qed "max_is_sup";
 
 
@@ -153,21 +153,21 @@
 goalw thy [is_inf_def, is_Inf_def] "is_Inf {x, y} inf = is_inf x y inf";
   br iffI 1;
   (*==>*)
-    by (fast_tac set_cs 1);
+    by (Fast_tac 1);
   (*<==*)
-    by (safe_tac set_cs);
-    by (step_tac set_cs 1);
+    by (safe_tac (!claset));
+    by (Step_tac 1);
     be mp 1;
-    by (fast_tac set_cs 1);
+    by (Fast_tac 1);
 qed "bin_is_Inf_eq";
 
 goalw thy [is_sup_def, is_Sup_def] "is_Sup {x, y} sup = is_sup x y sup";
   br iffI 1;
   (*==>*)
-    by (fast_tac set_cs 1);
+    by (Fast_tac 1);
   (*<==*)
-    by (safe_tac set_cs);
-    by (step_tac set_cs 1);
+    by (safe_tac (!claset));
+    by (Step_tac 1);
     be mp 1;
-    by (fast_tac set_cs 1);
+    by (Fast_tac 1);
 qed "bin_is_Sup_eq";
diff -r 260a9711f507 -r 0075a8d26a80 src/HOL/AxClasses/Lattice/tools.ML
--- a/src/HOL/AxClasses/Lattice/tools.ML	Fri Aug 02 12:16:11 1996 +0200
+++ b/src/HOL/AxClasses/Lattice/tools.ML	Fri Aug 02 12:25:26 1996 +0200
@@ -6,5 +6,5 @@
 qed "selectI1";
 
 goal HOL.thy "(P & Q) = (Q & P)";
-  by (fast_tac prop_cs 1);
+  by (Fast_tac 1);
 qed "conj_commut";
diff -r 260a9711f507 -r 0075a8d26a80 src/HOL/AxClasses/Tutorial/Xor.ML
--- a/src/HOL/AxClasses/Tutorial/Xor.ML	Fri Aug 02 12:16:11 1996 +0200
+++ b/src/HOL/AxClasses/Tutorial/Xor.ML	Fri Aug 02 12:25:26 1996 +0200
@@ -10,5 +10,5 @@
 goal_arity Xor.thy ("bool", [], "agroup");
 by (axclass_tac Xor.thy []);
 by (rewrite_goals_tac [Xor.prod_bool_def, Xor.inv_bool_def, Xor.unit_bool_def]);
-by (ALLGOALS (fast_tac HOL_cs));
+by (ALLGOALS (Fast_tac));
 qed "bool_in_agroup";