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