src/HOL/AxClasses/Lattice/Order.ML

--- a/src/HOL/AxClasses/Lattice/Order.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/Order.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -45,70 +45,70 @@
 (* 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 (claset()));
+  by Safe_tac;
   (*level 1*)
-    br (le_trans RS mp) 1;
-    be conjI 1;
-    ba 1;
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
+    by (assume_tac 1);
   (*level 4*)
     by (Step_tac 1);
     back();
-    be mp 1;
-    br conjI 1;
-    br (le_trans RS mp) 1;
-    be conjI 1;
-    ba 1;
-    ba 1;
+    by (etac mp 1);
+    by (rtac conjI 1);
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
+    by (assume_tac 1);
+    by (assume_tac 1);
   (*level 11*)
     by (Step_tac 1);
     back();
     back();
-    be mp 1;
-    br conjI 1;
+    by (etac mp 1);
+    by (rtac conjI 1);
     by (Step_tac 1);
-    be mp 1;
-    be conjI 1;
-    br (le_trans RS mp) 1;
-    be conjI 1;
-    ba 1;
-    br (le_trans RS mp) 1;
-    be conjI 1;
+    by (etac mp 1);
+    by (etac conjI 1);
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
+    by (assume_tac 1);
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
     back();     (* !! *)
-    ba 1;
+    by (assume_tac 1);
 qed "is_inf_assoc";
 
 
 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 (claset()));
+  by Safe_tac;
   (*level 1*)
-    br (le_trans RS mp) 1;
-    be conjI 1;
-    ba 1;
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
+    by (assume_tac 1);
   (*level 4*)
     by (Step_tac 1);
     back();
-    be mp 1;
-    br conjI 1;
-    br (le_trans RS mp) 1;
-    be conjI 1;
-    ba 1;
-    ba 1;
+    by (etac mp 1);
+    by (rtac conjI 1);
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
+    by (assume_tac 1);
+    by (assume_tac 1);
   (*level 11*)
     by (Step_tac 1);
     back();
     back();
-    be mp 1;
-    br conjI 1;
+    by (etac mp 1);
+    by (rtac conjI 1);
     by (Step_tac 1);
-    be mp 1;
-    be conjI 1;
-    br (le_trans RS mp) 1;
-    be conjI 1;
+    by (etac mp 1);
+    by (etac conjI 1);
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
     back();     (* !! *)
-    ba 1;
-    br (le_trans RS mp) 1;
-    be conjI 1;
-    ba 1;
+    by (assume_tac 1);
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
+    by (assume_tac 1);
 qed "is_sup_assoc";
 
 
@@ -118,15 +118,15 @@
   by (stac expand_if 1);
   by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   (*case "x [= y"*)
-    br le_refl 1;
-    ba 1;
+    by (rtac le_refl 1);
+    by (assume_tac 1);
     by (Fast_tac 1);
   (*case "~ x [= y"*)
-    br (le_linear RS disjE) 1;
-    ba 1;
-    be notE 1;
-    ba 1;
-    br le_refl 1;
+    by (rtac (le_linear RS disjE) 1);
+    by (assume_tac 1);
+    by (etac notE 1);
+    by (assume_tac 1);
+    by (rtac le_refl 1);
     by (Fast_tac 1);
 qed "min_is_inf";
 
@@ -134,15 +134,15 @@
   by (stac expand_if 1);
   by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   (*case "x [= y"*)
-    ba 1;
-    br le_refl 1;
+    by (assume_tac 1);
+    by (rtac le_refl 1);
     by (Fast_tac 1);
   (*case "~ x [= y"*)
-    br le_refl 1;
-    br (le_linear RS disjE) 1;
-    ba 1;
-    be notE 1;
-    ba 1;
+    by (rtac le_refl 1);
+    by (rtac (le_linear RS disjE) 1);
+    by (assume_tac 1);
+    by (etac notE 1);
+    by (assume_tac 1);
     by (Fast_tac 1);
 qed "max_is_sup";
 
@@ -151,23 +151,23 @@
 (** general vs. binary limits **)
 
 goalw thy [is_inf_def, is_Inf_def] "is_Inf {x, y} inf = is_inf x y inf";
-  br iffI 1;
+  by (rtac iffI 1);
   (*==>*)
     by (Fast_tac 1);
   (*<==*)
-    by (safe_tac (claset()));
+    by Safe_tac;
     by (Step_tac 1);
-    be mp 1;
+    by (etac mp 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 (rtac iffI 1);
   (*==>*)
     by (Fast_tac 1);
   (*<==*)
-    by (safe_tac (claset()));
+    by Safe_tac;
     by (Step_tac 1);
-    be mp 1;
+    by (etac mp 1);
     by (Fast_tac 1);
 qed "bin_is_Sup_eq";