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;