Classical tactics now use default claset.
authorberghofe
Fri Aug 02 12:25:26 1996 +0200 (1996-08-02)
changeset 18990075a8d26a80
parent 1898 260a9711f507
child 1900 c7a869229091
Classical tactics now use default claset.
src/HOL/AxClasses/Group/GroupDefs.ML
src/HOL/AxClasses/Lattice/CLattice.ML
src/HOL/AxClasses/Lattice/LatInsts.ML
src/HOL/AxClasses/Lattice/LatMorph.ML
src/HOL/AxClasses/Lattice/LatPreInsts.ML
src/HOL/AxClasses/Lattice/Lattice.ML
src/HOL/AxClasses/Lattice/OrdDefs.ML
src/HOL/AxClasses/Lattice/Order.ML
src/HOL/AxClasses/Lattice/tools.ML
src/HOL/AxClasses/Tutorial/Xor.ML
     1.1 --- a/src/HOL/AxClasses/Group/GroupDefs.ML	Fri Aug 02 12:16:11 1996 +0200
     1.2 +++ b/src/HOL/AxClasses/Group/GroupDefs.ML	Fri Aug 02 12:25:26 1996 +0200
     1.3 @@ -7,23 +7,23 @@
     1.4  (*this is really overkill - should be rather proven 'inline'*)
     1.5  
     1.6  goalw thy [times_bool_def] "(x * y) * z = x * (y * (z::bool))";
     1.7 -by (fast_tac HOL_cs 1);
     1.8 +by (Fast_tac 1);
     1.9  qed "bool_assoc";
    1.10  
    1.11  goalw thy [times_bool_def, one_bool_def] "1 * x = (x::bool)";
    1.12 -by (fast_tac HOL_cs 1);
    1.13 +by (Fast_tac 1);
    1.14  qed "bool_left_unit";
    1.15  
    1.16  goalw thy [times_bool_def, one_bool_def] "x * 1 = (x::bool)";
    1.17 -by (fast_tac HOL_cs 1);
    1.18 +by (Fast_tac 1);
    1.19  qed "bool_right_unit";
    1.20  
    1.21  goalw thy [times_bool_def, inv_bool_def, one_bool_def] "inv(x) * x = (1::bool)";
    1.22 -by (fast_tac HOL_cs 1);
    1.23 +by (Fast_tac 1);
    1.24  qed "bool_left_inv";
    1.25  
    1.26  goalw thy [times_bool_def] "x * y = (y * (x::bool))";
    1.27 -by (fast_tac HOL_cs 1);
    1.28 +by (Fast_tac 1);
    1.29  qed "bool_commut";
    1.30  
    1.31  
     2.1 --- a/src/HOL/AxClasses/Lattice/CLattice.ML	Fri Aug 02 12:16:11 1996 +0200
     2.2 +++ b/src/HOL/AxClasses/Lattice/CLattice.ML	Fri Aug 02 12:25:26 1996 +0200
     2.3 @@ -19,9 +19,9 @@
     2.4  qed "Inf_uniq";
     2.5  
     2.6  goalw thy [Ex1_def] "ALL A. EX! inf::'a::clattice. is_Inf A inf";
     2.7 -  by (safe_tac HOL_cs);
     2.8 -  by (step_tac HOL_cs 1);
     2.9 -  by (step_tac HOL_cs 1);
    2.10 +  by (safe_tac (!claset));
    2.11 +  by (Step_tac 1);
    2.12 +  by (Step_tac 1);
    2.13    br Inf_is_Inf 1;
    2.14    br (Inf_uniq RS mp RS sym) 1;
    2.15    ba 1;
    2.16 @@ -41,9 +41,9 @@
    2.17  qed "Sup_uniq";
    2.18  
    2.19  goalw thy [Ex1_def] "ALL A. EX! sup::'a::clattice. is_Sup A sup";
    2.20 -  by (safe_tac HOL_cs);
    2.21 -  by (step_tac HOL_cs 1);
    2.22 -  by (step_tac HOL_cs 1);
    2.23 +  by (safe_tac (!claset));
    2.24 +  by (Step_tac 1);
    2.25 +  by (Step_tac 1);
    2.26    br Sup_is_Sup 1;
    2.27    br (Sup_uniq RS mp RS sym) 1;
    2.28    ba 1;
    2.29 @@ -57,15 +57,15 @@
    2.30    br selectI2 1;
    2.31    br Inf_is_Inf 1;
    2.32    by (rewtac is_Inf_def);
    2.33 -  by (fast_tac set_cs 1);
    2.34 +  by (Fast_tac 1);
    2.35  qed "Inf_lb";
    2.36  
    2.37  val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A";
    2.38    br selectI2 1;
    2.39    br Inf_is_Inf 1;
    2.40    by (rewtac is_Inf_def);
    2.41 -  by (step_tac HOL_cs 1);
    2.42 -  by (step_tac HOL_cs 1);
    2.43 +  by (Step_tac 1);
    2.44 +  by (Step_tac 1);
    2.45    be mp 1;
    2.46    br ballI 1;
    2.47    be prem 1;
    2.48 @@ -77,15 +77,15 @@
    2.49    br selectI2 1;
    2.50    br Sup_is_Sup 1;
    2.51    by (rewtac is_Sup_def);
    2.52 -  by (fast_tac set_cs 1);
    2.53 +  by (Fast_tac 1);
    2.54  qed "Sup_ub";
    2.55  
    2.56  val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z";
    2.57    br selectI2 1;
    2.58    br Sup_is_Sup 1;
    2.59    by (rewtac is_Sup_def);
    2.60 -  by (step_tac HOL_cs 1);
    2.61 -  by (step_tac HOL_cs 1);
    2.62 +  by (Step_tac 1);
    2.63 +  by (Step_tac 1);
    2.64    be mp 1;
    2.65    br ballI 1;
    2.66    be prem 1;
    2.67 @@ -103,7 +103,7 @@
    2.68      be Inf_lb 1;
    2.69    (*<==*)
    2.70      br Inf_ub_lbs 1;
    2.71 -    by (fast_tac set_cs 1);
    2.72 +    by (Fast_tac 1);
    2.73  qed "le_Inf_eq";
    2.74  
    2.75  goal thy "(Sup A [= x) = (ALL y:A. y [= x)";
    2.76 @@ -116,7 +116,7 @@
    2.77      ba 1;
    2.78    (*<==*)
    2.79      br Sup_lb_ubs 1;
    2.80 -    by (fast_tac set_cs 1);
    2.81 +    by (Fast_tac 1);
    2.82  qed "ge_Sup_eq";
    2.83  
    2.84  
    2.85 @@ -127,7 +127,7 @@
    2.86    br impI 1;
    2.87    by (stac le_Inf_eq 1);
    2.88    by (rewtac Ball_def);
    2.89 -  by (safe_tac set_cs);
    2.90 +  by (safe_tac (!claset));
    2.91    bd subsetD 1;
    2.92    ba 1;
    2.93    be Inf_lb 1;
    2.94 @@ -137,7 +137,7 @@
    2.95    br impI 1;
    2.96    by (stac ge_Sup_eq 1);
    2.97    by (rewtac Ball_def);
    2.98 -  by (safe_tac set_cs);
    2.99 +  by (safe_tac (!claset));
   2.100    bd subsetD 1;
   2.101    ba 1;
   2.102    be Sup_ub 1;
   2.103 @@ -149,35 +149,35 @@
   2.104  goal thy "Inf {x} = x";
   2.105    br (Inf_uniq RS mp) 1;
   2.106    by (rewtac is_Inf_def);
   2.107 -  by (safe_tac set_cs);
   2.108 +  by (safe_tac (!claset));
   2.109    br le_refl 1;
   2.110 -  by (fast_tac set_cs 1);
   2.111 +  by (Fast_tac 1);
   2.112  qed "sing_Inf_eq";
   2.113  
   2.114  goal thy "Sup {x} = x";
   2.115    br (Sup_uniq RS mp) 1;
   2.116    by (rewtac is_Sup_def);
   2.117 -  by (safe_tac set_cs);
   2.118 +  by (safe_tac (!claset));
   2.119    br le_refl 1;
   2.120 -  by (fast_tac set_cs 1);
   2.121 +  by (Fast_tac 1);
   2.122  qed "sing_Sup_eq";
   2.123  
   2.124  
   2.125  goal thy "Inf {} = Sup {x. True}";
   2.126    br (Inf_uniq RS mp) 1;
   2.127    by (rewtac is_Inf_def);
   2.128 -  by (safe_tac set_cs);
   2.129 +  by (safe_tac (!claset));
   2.130    br (sing_Sup_eq RS subst) 1;
   2.131    back();
   2.132    br (Sup_subset_mon RS mp) 1;
   2.133 -  by (fast_tac set_cs 1);
   2.134 +  by (Fast_tac 1);
   2.135  qed "empty_Inf_eq";
   2.136  
   2.137  goal thy "Sup {} = Inf {x. True}";
   2.138    br (Sup_uniq RS mp) 1;
   2.139    by (rewtac is_Sup_def);
   2.140 -  by (safe_tac set_cs);
   2.141 +  by (safe_tac (!claset));
   2.142    br (sing_Inf_eq RS subst) 1;
   2.143    br (Inf_subset_antimon RS mp) 1;
   2.144 -  by (fast_tac set_cs 1);
   2.145 +  by (Fast_tac 1);
   2.146  qed "empty_Sup_eq";
     3.1 --- a/src/HOL/AxClasses/Lattice/LatInsts.ML	Fri Aug 02 12:16:11 1996 +0200
     3.2 +++ b/src/HOL/AxClasses/Lattice/LatInsts.ML	Fri Aug 02 12:25:26 1996 +0200
     3.3 @@ -21,7 +21,7 @@
     3.4  goal thy "Inf (A Un B) = Inf A && Inf B";
     3.5    br (Inf_uniq RS mp) 1;
     3.6    by (rewtac is_Inf_def);
     3.7 -  by (safe_tac set_cs);
     3.8 +  by (safe_tac (!claset));
     3.9  
    3.10    br (conjI RS (le_trans RS mp)) 1;
    3.11    br inf_lb1 1;
    3.12 @@ -34,26 +34,26 @@
    3.13    by (stac le_inf_eq 1);
    3.14    br conjI 1;
    3.15    br Inf_ub_lbs 1;
    3.16 -  by (fast_tac set_cs 1);
    3.17 +  by (Fast_tac 1);
    3.18    br Inf_ub_lbs 1;
    3.19 -  by (fast_tac set_cs 1);
    3.20 +  by (Fast_tac 1);
    3.21  qed "Inf_Un_eq";
    3.22  
    3.23  goal thy "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}";
    3.24    br (Inf_uniq RS mp) 1;
    3.25    by (rewtac is_Inf_def);
    3.26 -  by (safe_tac set_cs);
    3.27 +  by (safe_tac (!claset));
    3.28    (*level 3*)
    3.29    br (conjI RS (le_trans RS mp)) 1;
    3.30    be Inf_lb 2;
    3.31    br (sing_Inf_eq RS subst) 1;
    3.32    br (Inf_subset_antimon RS mp) 1;
    3.33 -  by (fast_tac set_cs 1);
    3.34 +  by (Fast_tac 1);
    3.35    (*level 8*)
    3.36    by (stac le_Inf_eq 1);
    3.37 -  by (safe_tac set_cs);
    3.38 +  by (safe_tac (!claset));
    3.39    by (stac le_Inf_eq 1);
    3.40 -  by (fast_tac set_cs 1);
    3.41 +  by (Fast_tac 1);
    3.42  qed "Inf_UN_eq";
    3.43  
    3.44  
    3.45 @@ -61,7 +61,7 @@
    3.46  goal thy "Sup (A Un B) = Sup A || Sup B";
    3.47    br (Sup_uniq RS mp) 1;
    3.48    by (rewtac is_Sup_def);
    3.49 -  by (safe_tac set_cs);
    3.50 +  by (safe_tac (!claset));
    3.51  
    3.52    br (conjI RS (le_trans RS mp)) 1;
    3.53    be Sup_ub 1;
    3.54 @@ -74,25 +74,25 @@
    3.55    by (stac ge_sup_eq 1);
    3.56    br conjI 1;
    3.57    br Sup_lb_ubs 1;
    3.58 -  by (fast_tac set_cs 1);
    3.59 +  by (Fast_tac 1);
    3.60    br Sup_lb_ubs 1;
    3.61 -  by (fast_tac set_cs 1);
    3.62 +  by (Fast_tac 1);
    3.63  qed "Sup_Un_eq";
    3.64  
    3.65  goal thy "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}";
    3.66    br (Sup_uniq RS mp) 1;
    3.67    by (rewtac is_Sup_def);
    3.68 -  by (safe_tac set_cs);
    3.69 +  by (safe_tac (!claset));
    3.70    (*level 3*)
    3.71    br (conjI RS (le_trans RS mp)) 1;
    3.72    be Sup_ub 1;
    3.73    br (sing_Sup_eq RS subst) 1;
    3.74    back();
    3.75    br (Sup_subset_mon RS mp) 1;
    3.76 -  by (fast_tac set_cs 1);
    3.77 +  by (Fast_tac 1);
    3.78    (*level 8*)
    3.79    by (stac ge_Sup_eq 1);
    3.80 -  by (safe_tac set_cs);
    3.81 +  by (safe_tac (!claset));
    3.82    by (stac ge_Sup_eq 1);
    3.83 -  by (fast_tac set_cs 1);
    3.84 +  by (Fast_tac 1);
    3.85  qed "Sup_UN_eq";
     4.1 --- a/src/HOL/AxClasses/Lattice/LatMorph.ML	Fri Aug 02 12:16:11 1996 +0200
     4.2 +++ b/src/HOL/AxClasses/Lattice/LatMorph.ML	Fri Aug 02 12:25:26 1996 +0200
     4.3 @@ -5,16 +5,16 @@
     4.4  (** monotone functions vs. "&&"- / "||"-semi-morphisms **)
     4.5  
     4.6  goalw thy [is_mono_def] "is_mono f = (ALL x y. f (x && y) [= f x && f y)";
     4.7 -  by (safe_tac set_cs);
     4.8 +  by (safe_tac (!claset));
     4.9    (*==> (level 1)*)
    4.10      by (stac le_inf_eq 1);
    4.11      br conjI 1;
    4.12 -    by (step_tac set_cs 1);
    4.13 -    by (step_tac set_cs 1);
    4.14 +    by (Step_tac 1);
    4.15 +    by (Step_tac 1);
    4.16      be mp 1;
    4.17      br inf_lb1 1;
    4.18 -    by (step_tac set_cs 1);
    4.19 -    by (step_tac set_cs 1);
    4.20 +    by (Step_tac 1);
    4.21 +    by (Step_tac 1);
    4.22      be mp 1;
    4.23      br inf_lb2 1;
    4.24    (*==> (level 11)*)
    4.25 @@ -22,22 +22,22 @@
    4.26      br inf_lb2 2;
    4.27      by (subgoal_tac "x && y = x" 1);
    4.28      be subst 1;
    4.29 -    by (fast_tac set_cs 1);
    4.30 +    by (Fast_tac 1);
    4.31      by (stac inf_connect 1);
    4.32      ba 1;
    4.33  qed "mono_inf_eq";
    4.34  
    4.35  goalw thy [is_mono_def] "is_mono f = (ALL x y. f x || f y [= f (x || y))";
    4.36 -  by (safe_tac set_cs);
    4.37 +  by (safe_tac (!claset));
    4.38    (*==> (level 1)*)
    4.39      by (stac ge_sup_eq 1);
    4.40      br conjI 1;
    4.41 -    by (step_tac set_cs 1);
    4.42 -    by (step_tac set_cs 1);
    4.43 +    by (Step_tac 1);
    4.44 +    by (Step_tac 1);
    4.45      be mp 1;
    4.46      br sup_ub1 1;
    4.47 -    by (step_tac set_cs 1);
    4.48 -    by (step_tac set_cs 1);
    4.49 +    by (Step_tac 1);
    4.50 +    by (Step_tac 1);
    4.51      be mp 1;
    4.52      br sup_ub2 1;
    4.53    (*==> (level 11)*)
    4.54 @@ -45,7 +45,7 @@
    4.55      br sup_ub1 1;
    4.56      by (subgoal_tac "x || y = y" 1);
    4.57      be subst 1;
    4.58 -    by (fast_tac set_cs 1);
    4.59 +    by (Fast_tac 1);
    4.60      by (stac sup_connect 1);
    4.61      ba 1;
    4.62  qed "mono_sup_eq";
     5.1 --- a/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Fri Aug 02 12:16:11 1996 +0200
     5.2 +++ b/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Fri Aug 02 12:25:26 1996 +0200
     5.3 @@ -22,13 +22,13 @@
     5.4  
     5.5  goalw thy [is_inf_def, le_prod_def] "is_inf p q (fst p && fst q, snd p && snd q)";
     5.6    by (Simp_tac 1);
     5.7 -  by (safe_tac HOL_cs);
     5.8 +  by (safe_tac (!claset));
     5.9    by (REPEAT_FIRST (fn i => resolve_tac [inf_lb1, inf_lb2, inf_ub_lbs] i ORELSE atac i));
    5.10  qed "prod_is_inf";
    5.11  
    5.12  goalw thy [is_sup_def, le_prod_def] "is_sup p q (fst p || fst q, snd p || snd q)";
    5.13    by (Simp_tac 1);
    5.14 -  by (safe_tac HOL_cs);
    5.15 +  by (safe_tac (!claset));
    5.16    by (REPEAT_FIRST (fn i => resolve_tac [sup_ub1, sup_ub2, sup_lb_ubs] i ORELSE atac i));
    5.17  qed "prod_is_sup";
    5.18  
    5.19 @@ -36,19 +36,19 @@
    5.20  (* functions *)
    5.21  
    5.22  goalw thy [is_inf_def, le_fun_def] "is_inf f g (%x. f x && g x)";
    5.23 -  by (safe_tac HOL_cs);
    5.24 +  by (safe_tac (!claset));
    5.25    br inf_lb1 1;
    5.26    br inf_lb2 1;
    5.27    br inf_ub_lbs 1;
    5.28 -  by (REPEAT_FIRST (fast_tac HOL_cs));
    5.29 +  by (REPEAT_FIRST (Fast_tac));
    5.30  qed "fun_is_inf";
    5.31  
    5.32  goalw thy [is_sup_def, le_fun_def] "is_sup f g (%x. f x || g x)";
    5.33 -  by (safe_tac HOL_cs);
    5.34 +  by (safe_tac (!claset));
    5.35    br sup_ub1 1;
    5.36    br sup_ub2 1;
    5.37    br sup_lb_ubs 1;
    5.38 -  by (REPEAT_FIRST (fast_tac HOL_cs));
    5.39 +  by (REPEAT_FIRST (Fast_tac));
    5.40  qed "fun_is_sup";
    5.41  
    5.42  
    5.43 @@ -57,7 +57,7 @@
    5.44  
    5.45  goalw thy [is_inf_def, le_dual_def] "is_inf x y (Abs_dual (Rep_dual x || Rep_dual y))";
    5.46    by (stac Abs_dual_inverse' 1);
    5.47 -  by (safe_tac HOL_cs);
    5.48 +  by (safe_tac (!claset));
    5.49    br sup_ub1 1;
    5.50    br sup_ub2 1;
    5.51    br sup_lb_ubs 1;
    5.52 @@ -67,7 +67,7 @@
    5.53  
    5.54  goalw thy [is_sup_def, le_dual_def] "is_sup x y (Abs_dual (Rep_dual x && Rep_dual y))";
    5.55    by (stac Abs_dual_inverse' 1);
    5.56 -  by (safe_tac HOL_cs);
    5.57 +  by (safe_tac (!claset));
    5.58    br inf_lb1 1;
    5.59    br inf_lb2 1;
    5.60    br inf_ub_lbs 1;
     6.1 --- a/src/HOL/AxClasses/Lattice/Lattice.ML	Fri Aug 02 12:16:11 1996 +0200
     6.2 +++ b/src/HOL/AxClasses/Lattice/Lattice.ML	Fri Aug 02 12:25:26 1996 +0200
     6.3 @@ -19,9 +19,9 @@
     6.4  qed "inf_uniq";
     6.5  
     6.6  goalw thy [Ex1_def] "ALL x y. EX! inf::'a::lattice. is_inf x y inf";
     6.7 -  by (safe_tac HOL_cs);
     6.8 -  by (step_tac HOL_cs 1);
     6.9 -  by (step_tac HOL_cs 1);
    6.10 +  by (safe_tac (!claset));
    6.11 +  by (Step_tac 1);
    6.12 +  by (Step_tac 1);
    6.13    br inf_is_inf 1;
    6.14    br (inf_uniq RS mp RS sym) 1;
    6.15    ba 1;
    6.16 @@ -41,9 +41,9 @@
    6.17  qed "sup_uniq";
    6.18  
    6.19  goalw thy [Ex1_def] "ALL x y. EX! sup::'a::lattice. is_sup x y sup";
    6.20 -  by (safe_tac HOL_cs);
    6.21 -  by (step_tac HOL_cs 1);
    6.22 -  by (step_tac HOL_cs 1);
    6.23 +  by (safe_tac (!claset));
    6.24 +  by (Step_tac 1);
    6.25 +  by (Step_tac 1);
    6.26    br sup_is_sup 1;
    6.27    br (sup_uniq RS mp RS sym) 1;
    6.28    ba 1;
    6.29 @@ -55,7 +55,7 @@
    6.30  val tac =
    6.31    cut_facts_tac [inf_is_inf] 1 THEN
    6.32    rewrite_goals_tac [inf_def, is_inf_def] THEN
    6.33 -  fast_tac HOL_cs 1;
    6.34 +  Fast_tac 1;
    6.35  
    6.36  goal thy "x && y [= x";
    6.37    by tac;
    6.38 @@ -74,7 +74,7 @@
    6.39  val tac =
    6.40    cut_facts_tac [sup_is_sup] 1 THEN
    6.41    rewrite_goals_tac [sup_def, is_sup_def] THEN
    6.42 -  fast_tac HOL_cs 1;
    6.43 +  Fast_tac 1;
    6.44  
    6.45  goal thy "x [= x || y";
    6.46    by tac;
    6.47 @@ -106,7 +106,7 @@
    6.48      by (REPEAT_FIRST (rtac conjI));
    6.49      br le_refl 1;
    6.50      ba 1;
    6.51 -    by (fast_tac HOL_cs 1);
    6.52 +    by (Fast_tac 1);
    6.53  qed "inf_connect";
    6.54  
    6.55  goal thy "(x || y = y) = (x [= y)";
    6.56 @@ -120,7 +120,7 @@
    6.57      by (REPEAT_FIRST (rtac conjI));
    6.58      ba 1;
    6.59      br le_refl 1;
    6.60 -    by (fast_tac HOL_cs 1);
    6.61 +    by (Fast_tac 1);
    6.62  qed "sup_connect";
    6.63  
    6.64  
     7.1 --- a/src/HOL/AxClasses/Lattice/OrdDefs.ML	Fri Aug 02 12:16:11 1996 +0200
     7.2 +++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML	Fri Aug 02 12:25:26 1996 +0200
     7.3 @@ -13,7 +13,7 @@
     7.4  qed "le_prod_refl";
     7.5  
     7.6  goalw thy [le_prod_def] "x [= y & y [= z --> x [= (z::'a::quasi_order*'b::quasi_order)";
     7.7 -  by (safe_tac HOL_cs);
     7.8 +  by (safe_tac (!claset));
     7.9    be (conjI RS (le_trans RS mp)) 1;
    7.10    ba 1;
    7.11    be (conjI RS (le_trans RS mp)) 1;
    7.12 @@ -21,7 +21,7 @@
    7.13  qed "le_prod_trans";
    7.14  
    7.15  goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::order*'b::order)";
    7.16 -  by (safe_tac HOL_cs);
    7.17 +  by (safe_tac (!claset));
    7.18    by (stac Pair_fst_snd_eq 1);
    7.19    br conjI 1;
    7.20    be (conjI RS (le_antisym RS mp)) 1;
    7.21 @@ -39,16 +39,16 @@
    7.22  qed "le_fun_refl";
    7.23  
    7.24  goalw thy [le_fun_def] "f [= g & g [= h --> f [= (h::'a=>'b::quasi_order)";
    7.25 -  by (safe_tac HOL_cs);
    7.26 +  by (safe_tac (!claset));
    7.27    br (le_trans RS mp) 1;
    7.28 -  by (fast_tac HOL_cs 1);
    7.29 +  by (Fast_tac 1);
    7.30  qed "le_fun_trans";
    7.31  
    7.32  goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::order)";
    7.33 -  by (safe_tac HOL_cs);
    7.34 +  by (safe_tac (!claset));
    7.35    br ext 1;
    7.36    br (le_antisym RS mp) 1;
    7.37 -  by (fast_tac HOL_cs 1);
    7.38 +  by (Fast_tac 1);
    7.39  qed "le_fun_antisym";
    7.40  
    7.41  
    7.42 @@ -59,7 +59,7 @@
    7.43  goal thy "Rep_dual (Abs_dual y) = y";
    7.44    br Abs_dual_inverse 1;
    7.45    by (rewtac dual_def);
    7.46 -  by (fast_tac set_cs 1);
    7.47 +  by (Fast_tac 1);
    7.48  qed "Abs_dual_inverse'";
    7.49  
    7.50  
    7.51 @@ -73,7 +73,7 @@
    7.52  qed "le_dual_trans";
    7.53  
    7.54  goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::order dual)";
    7.55 -  by (safe_tac prop_cs);
    7.56 +  by (safe_tac (!claset));
    7.57    br (Rep_dual_inverse RS subst) 1;
    7.58    br sym 1;
    7.59    br (Rep_dual_inverse RS subst) 1;
     8.1 --- a/src/HOL/AxClasses/Lattice/Order.ML	Fri Aug 02 12:16:11 1996 +0200
     8.2 +++ b/src/HOL/AxClasses/Lattice/Order.ML	Fri Aug 02 12:25:26 1996 +0200
     8.3 @@ -9,7 +9,7 @@
     8.4  val tac =
     8.5    rtac impI 1 THEN
     8.6    rtac (le_antisym RS mp) 1 THEN
     8.7 -  fast_tac HOL_cs 1;
     8.8 +  Fast_tac 1;
     8.9  
    8.10  
    8.11  goalw thy [is_inf_def] "is_inf x y inf & is_inf x y inf' --> inf = inf'";
    8.12 @@ -34,24 +34,24 @@
    8.13  (* commutativity *)
    8.14  
    8.15  goalw thy [is_inf_def] "is_inf x y inf = is_inf y x inf";
    8.16 -  by (fast_tac HOL_cs 1);
    8.17 +  by (Fast_tac 1);
    8.18  qed "is_inf_commut";
    8.19  
    8.20  goalw thy [is_sup_def] "is_sup x y sup = is_sup y x sup";
    8.21 -  by (fast_tac HOL_cs 1);
    8.22 +  by (Fast_tac 1);
    8.23  qed "is_sup_commut";
    8.24  
    8.25  
    8.26  (* associativity *)
    8.27  
    8.28  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";
    8.29 -  by (safe_tac HOL_cs);
    8.30 +  by (safe_tac (!claset));
    8.31    (*level 1*)
    8.32      br (le_trans RS mp) 1;
    8.33      be conjI 1;
    8.34      ba 1;
    8.35    (*level 4*)
    8.36 -    by (step_tac HOL_cs 1);
    8.37 +    by (Step_tac 1);
    8.38      back();
    8.39      be mp 1;
    8.40      br conjI 1;
    8.41 @@ -60,12 +60,12 @@
    8.42      ba 1;
    8.43      ba 1;
    8.44    (*level 11*)
    8.45 -    by (step_tac HOL_cs 1);
    8.46 +    by (Step_tac 1);
    8.47      back();
    8.48      back();
    8.49      be mp 1;
    8.50      br conjI 1;
    8.51 -    by (step_tac HOL_cs 1);
    8.52 +    by (Step_tac 1);
    8.53      be mp 1;
    8.54      be conjI 1;
    8.55      br (le_trans RS mp) 1;
    8.56 @@ -79,13 +79,13 @@
    8.57  
    8.58  
    8.59  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";
    8.60 -  by (safe_tac HOL_cs);
    8.61 +  by (safe_tac (!claset));
    8.62    (*level 1*)
    8.63      br (le_trans RS mp) 1;
    8.64      be conjI 1;
    8.65      ba 1;
    8.66    (*level 4*)
    8.67 -    by (step_tac HOL_cs 1);
    8.68 +    by (Step_tac 1);
    8.69      back();
    8.70      be mp 1;
    8.71      br conjI 1;
    8.72 @@ -94,12 +94,12 @@
    8.73      ba 1;
    8.74      ba 1;
    8.75    (*level 11*)
    8.76 -    by (step_tac HOL_cs 1);
    8.77 +    by (Step_tac 1);
    8.78      back();
    8.79      back();
    8.80      be mp 1;
    8.81      br conjI 1;
    8.82 -    by (step_tac HOL_cs 1);
    8.83 +    by (Step_tac 1);
    8.84      be mp 1;
    8.85      be conjI 1;
    8.86      br (le_trans RS mp) 1;
    8.87 @@ -120,14 +120,14 @@
    8.88    (*case "x [= y"*)
    8.89      br le_refl 1;
    8.90      ba 1;
    8.91 -    by (fast_tac HOL_cs 1);
    8.92 +    by (Fast_tac 1);
    8.93    (*case "~ x [= y"*)
    8.94      br (le_lin RS disjE) 1;
    8.95      ba 1;
    8.96      be notE 1;
    8.97      ba 1;
    8.98      br le_refl 1;
    8.99 -    by (fast_tac HOL_cs 1);
   8.100 +    by (Fast_tac 1);
   8.101  qed "min_is_inf";
   8.102  
   8.103  goalw thy [maximum_def, is_sup_def] "is_sup (x::'a::lin_order) y (maximum x y)";
   8.104 @@ -136,14 +136,14 @@
   8.105    (*case "x [= y"*)
   8.106      ba 1;
   8.107      br le_refl 1;
   8.108 -    by (fast_tac HOL_cs 1);
   8.109 +    by (Fast_tac 1);
   8.110    (*case "~ x [= y"*)
   8.111      br le_refl 1;
   8.112      br (le_lin RS disjE) 1;
   8.113      ba 1;
   8.114      be notE 1;
   8.115      ba 1;
   8.116 -    by (fast_tac HOL_cs 1);
   8.117 +    by (Fast_tac 1);
   8.118  qed "max_is_sup";
   8.119  
   8.120  
   8.121 @@ -153,21 +153,21 @@
   8.122  goalw thy [is_inf_def, is_Inf_def] "is_Inf {x, y} inf = is_inf x y inf";
   8.123    br iffI 1;
   8.124    (*==>*)
   8.125 -    by (fast_tac set_cs 1);
   8.126 +    by (Fast_tac 1);
   8.127    (*<==*)
   8.128 -    by (safe_tac set_cs);
   8.129 -    by (step_tac set_cs 1);
   8.130 +    by (safe_tac (!claset));
   8.131 +    by (Step_tac 1);
   8.132      be mp 1;
   8.133 -    by (fast_tac set_cs 1);
   8.134 +    by (Fast_tac 1);
   8.135  qed "bin_is_Inf_eq";
   8.136  
   8.137  goalw thy [is_sup_def, is_Sup_def] "is_Sup {x, y} sup = is_sup x y sup";
   8.138    br iffI 1;
   8.139    (*==>*)
   8.140 -    by (fast_tac set_cs 1);
   8.141 +    by (Fast_tac 1);
   8.142    (*<==*)
   8.143 -    by (safe_tac set_cs);
   8.144 -    by (step_tac set_cs 1);
   8.145 +    by (safe_tac (!claset));
   8.146 +    by (Step_tac 1);
   8.147      be mp 1;
   8.148 -    by (fast_tac set_cs 1);
   8.149 +    by (Fast_tac 1);
   8.150  qed "bin_is_Sup_eq";
     9.1 --- a/src/HOL/AxClasses/Lattice/tools.ML	Fri Aug 02 12:16:11 1996 +0200
     9.2 +++ b/src/HOL/AxClasses/Lattice/tools.ML	Fri Aug 02 12:25:26 1996 +0200
     9.3 @@ -6,5 +6,5 @@
     9.4  qed "selectI1";
     9.5  
     9.6  goal HOL.thy "(P & Q) = (Q & P)";
     9.7 -  by (fast_tac prop_cs 1);
     9.8 +  by (Fast_tac 1);
     9.9  qed "conj_commut";
    10.1 --- a/src/HOL/AxClasses/Tutorial/Xor.ML	Fri Aug 02 12:16:11 1996 +0200
    10.2 +++ b/src/HOL/AxClasses/Tutorial/Xor.ML	Fri Aug 02 12:25:26 1996 +0200
    10.3 @@ -10,5 +10,5 @@
    10.4  goal_arity Xor.thy ("bool", [], "agroup");
    10.5  by (axclass_tac Xor.thy []);
    10.6  by (rewrite_goals_tac [Xor.prod_bool_def, Xor.inv_bool_def, Xor.unit_bool_def]);
    10.7 -by (ALLGOALS (fast_tac HOL_cs));
    10.8 +by (ALLGOALS (Fast_tac));
    10.9  qed "bool_in_agroup";