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";