1.1 --- a/src/HOL/AxClasses/Lattice/OrdDefs.ML	Fri Aug 02 12:16:11 1996 +0200
     1.2 +++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML	Fri Aug 02 12:25:26 1996 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  qed "le_prod_refl";
     1.5  
     1.6  goalw thy [le_prod_def] "x [= y & y [= z --> x [= (z::'a::quasi_order*'b::quasi_order)";
     1.7 -  by (safe_tac HOL_cs);
     1.8 +  by (safe_tac (!claset));
     1.9    be (conjI RS (le_trans RS mp)) 1;
    1.10    ba 1;
    1.11    be (conjI RS (le_trans RS mp)) 1;
    1.12 @@ -21,7 +21,7 @@
    1.13  qed "le_prod_trans";
    1.14  
    1.15  goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::order*'b::order)";
    1.16 -  by (safe_tac HOL_cs);
    1.17 +  by (safe_tac (!claset));
    1.18    by (stac Pair_fst_snd_eq 1);
    1.19    br conjI 1;
    1.20    be (conjI RS (le_antisym RS mp)) 1;
    1.21 @@ -39,16 +39,16 @@
    1.22  qed "le_fun_refl";
    1.23  
    1.24  goalw thy [le_fun_def] "f [= g & g [= h --> f [= (h::'a=>'b::quasi_order)";
    1.25 -  by (safe_tac HOL_cs);
    1.26 +  by (safe_tac (!claset));
    1.27    br (le_trans RS mp) 1;
    1.28 -  by (fast_tac HOL_cs 1);
    1.29 +  by (Fast_tac 1);
    1.30  qed "le_fun_trans";
    1.31  
    1.32  goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::order)";
    1.33 -  by (safe_tac HOL_cs);
    1.34 +  by (safe_tac (!claset));
    1.35    br ext 1;
    1.36    br (le_antisym RS mp) 1;
    1.37 -  by (fast_tac HOL_cs 1);
    1.38 +  by (Fast_tac 1);
    1.39  qed "le_fun_antisym";
    1.40  
    1.41  
    1.42 @@ -59,7 +59,7 @@
    1.43  goal thy "Rep_dual (Abs_dual y) = y";
    1.44    br Abs_dual_inverse 1;
    1.45    by (rewtac dual_def);
    1.46 -  by (fast_tac set_cs 1);
    1.47 +  by (Fast_tac 1);
    1.48  qed "Abs_dual_inverse'";
    1.49  
    1.50  
    1.51 @@ -73,7 +73,7 @@
    1.52  qed "le_dual_trans";
    1.53  
    1.54  goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::order dual)";
    1.55 -  by (safe_tac prop_cs);
    1.56 +  by (safe_tac (!claset));
    1.57    br (Rep_dual_inverse RS subst) 1;
    1.58    br sym 1;
    1.59    br (Rep_dual_inverse RS subst) 1;