1.1 --- a/src/HOL/AxClasses/Lattice/Order.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/AxClasses/Lattice/Order.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -45,70 +45,70 @@
     1.4  (* associativity *)
     1.5  
     1.6  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";
     1.7 -  by (safe_tac (claset()));
     1.8 +  by Safe_tac;
     1.9    (*level 1*)
    1.10 -    br (le_trans RS mp) 1;
    1.11 -    be conjI 1;
    1.12 -    ba 1;
    1.13 +    by (rtac (le_trans RS mp) 1);
    1.14 +    by (etac conjI 1);
    1.15 +    by (assume_tac 1);
    1.16    (*level 4*)
    1.17      by (Step_tac 1);
    1.18      back();
    1.19 -    be mp 1;
    1.20 -    br conjI 1;
    1.21 -    br (le_trans RS mp) 1;
    1.22 -    be conjI 1;
    1.23 -    ba 1;
    1.24 -    ba 1;
    1.25 +    by (etac mp 1);
    1.26 +    by (rtac conjI 1);
    1.27 +    by (rtac (le_trans RS mp) 1);
    1.28 +    by (etac conjI 1);
    1.29 +    by (assume_tac 1);
    1.30 +    by (assume_tac 1);
    1.31    (*level 11*)
    1.32      by (Step_tac 1);
    1.33      back();
    1.34      back();
    1.35 -    be mp 1;
    1.36 -    br conjI 1;
    1.37 +    by (etac mp 1);
    1.38 +    by (rtac conjI 1);
    1.39      by (Step_tac 1);
    1.40 -    be mp 1;
    1.41 -    be conjI 1;
    1.42 -    br (le_trans RS mp) 1;
    1.43 -    be conjI 1;
    1.44 -    ba 1;
    1.45 -    br (le_trans RS mp) 1;
    1.46 -    be conjI 1;
    1.47 +    by (etac mp 1);
    1.48 +    by (etac conjI 1);
    1.49 +    by (rtac (le_trans RS mp) 1);
    1.50 +    by (etac conjI 1);
    1.51 +    by (assume_tac 1);
    1.52 +    by (rtac (le_trans RS mp) 1);
    1.53 +    by (etac conjI 1);
    1.54      back();     (* !! *)
    1.55 -    ba 1;
    1.56 +    by (assume_tac 1);
    1.57  qed "is_inf_assoc";
    1.58  
    1.59  
    1.60  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";
    1.61 -  by (safe_tac (claset()));
    1.62 +  by Safe_tac;
    1.63    (*level 1*)
    1.64 -    br (le_trans RS mp) 1;
    1.65 -    be conjI 1;
    1.66 -    ba 1;
    1.67 +    by (rtac (le_trans RS mp) 1);
    1.68 +    by (etac conjI 1);
    1.69 +    by (assume_tac 1);
    1.70    (*level 4*)
    1.71      by (Step_tac 1);
    1.72      back();
    1.73 -    be mp 1;
    1.74 -    br conjI 1;
    1.75 -    br (le_trans RS mp) 1;
    1.76 -    be conjI 1;
    1.77 -    ba 1;
    1.78 -    ba 1;
    1.79 +    by (etac mp 1);
    1.80 +    by (rtac conjI 1);
    1.81 +    by (rtac (le_trans RS mp) 1);
    1.82 +    by (etac conjI 1);
    1.83 +    by (assume_tac 1);
    1.84 +    by (assume_tac 1);
    1.85    (*level 11*)
    1.86      by (Step_tac 1);
    1.87      back();
    1.88      back();
    1.89 -    be mp 1;
    1.90 -    br conjI 1;
    1.91 +    by (etac mp 1);
    1.92 +    by (rtac conjI 1);
    1.93      by (Step_tac 1);
    1.94 -    be mp 1;
    1.95 -    be conjI 1;
    1.96 -    br (le_trans RS mp) 1;
    1.97 -    be conjI 1;
    1.98 +    by (etac mp 1);
    1.99 +    by (etac conjI 1);
   1.100 +    by (rtac (le_trans RS mp) 1);
   1.101 +    by (etac conjI 1);
   1.102      back();     (* !! *)
   1.103 -    ba 1;
   1.104 -    br (le_trans RS mp) 1;
   1.105 -    be conjI 1;
   1.106 -    ba 1;
   1.107 +    by (assume_tac 1);
   1.108 +    by (rtac (le_trans RS mp) 1);
   1.109 +    by (etac conjI 1);
   1.110 +    by (assume_tac 1);
   1.111  qed "is_sup_assoc";
   1.112  
   1.113  
   1.114 @@ -118,15 +118,15 @@
   1.115    by (stac expand_if 1);
   1.116    by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   1.117    (*case "x [= y"*)
   1.118 -    br le_refl 1;
   1.119 -    ba 1;
   1.120 +    by (rtac le_refl 1);
   1.121 +    by (assume_tac 1);
   1.122      by (Fast_tac 1);
   1.123    (*case "~ x [= y"*)
   1.124 -    br (le_linear RS disjE) 1;
   1.125 -    ba 1;
   1.126 -    be notE 1;
   1.127 -    ba 1;
   1.128 -    br le_refl 1;
   1.129 +    by (rtac (le_linear RS disjE) 1);
   1.130 +    by (assume_tac 1);
   1.131 +    by (etac notE 1);
   1.132 +    by (assume_tac 1);
   1.133 +    by (rtac le_refl 1);
   1.134      by (Fast_tac 1);
   1.135  qed "min_is_inf";
   1.136  
   1.137 @@ -134,15 +134,15 @@
   1.138    by (stac expand_if 1);
   1.139    by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   1.140    (*case "x [= y"*)
   1.141 -    ba 1;
   1.142 -    br le_refl 1;
   1.143 +    by (assume_tac 1);
   1.144 +    by (rtac le_refl 1);
   1.145      by (Fast_tac 1);
   1.146    (*case "~ x [= y"*)
   1.147 -    br le_refl 1;
   1.148 -    br (le_linear RS disjE) 1;
   1.149 -    ba 1;
   1.150 -    be notE 1;
   1.151 -    ba 1;
   1.152 +    by (rtac le_refl 1);
   1.153 +    by (rtac (le_linear RS disjE) 1);
   1.154 +    by (assume_tac 1);
   1.155 +    by (etac notE 1);
   1.156 +    by (assume_tac 1);
   1.157      by (Fast_tac 1);
   1.158  qed "max_is_sup";
   1.159  
   1.160 @@ -151,23 +151,23 @@
   1.161  (** general vs. binary limits **)
   1.162  
   1.163  goalw thy [is_inf_def, is_Inf_def] "is_Inf {x, y} inf = is_inf x y inf";
   1.164 -  br iffI 1;
   1.165 +  by (rtac iffI 1);
   1.166    (*==>*)
   1.167      by (Fast_tac 1);
   1.168    (*<==*)
   1.169 -    by (safe_tac (claset()));
   1.170 +    by Safe_tac;
   1.171      by (Step_tac 1);
   1.172 -    be mp 1;
   1.173 +    by (etac mp 1);
   1.174      by (Fast_tac 1);
   1.175  qed "bin_is_Inf_eq";
   1.176  
   1.177  goalw thy [is_sup_def, is_Sup_def] "is_Sup {x, y} sup = is_sup x y sup";
   1.178 -  br iffI 1;
   1.179 +  by (rtac iffI 1);
   1.180    (*==>*)
   1.181      by (Fast_tac 1);
   1.182    (*<==*)
   1.183 -    by (safe_tac (claset()));
   1.184 +    by Safe_tac;
   1.185      by (Step_tac 1);
   1.186 -    be mp 1;
   1.187 +    by (etac mp 1);
   1.188      by (Fast_tac 1);
   1.189  qed "bin_is_Sup_eq";