1.1 --- a/src/HOL/AxClasses/Lattice/LatMorph.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/AxClasses/Lattice/LatMorph.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -5,49 +5,49 @@
     1.4  (** monotone functions vs. "&&"- / "||"-semi-morphisms **)
     1.5  
     1.6  goalw thy [is_mono_def] "is_mono f = (ALL x y. f (x && y) [= f x && f y)";
     1.7 -  by (safe_tac (claset()));
     1.8 +  by Safe_tac;
     1.9    (*==> (level 1)*)
    1.10      by (stac le_inf_eq 1);
    1.11 -    br conjI 1;
    1.12 +    by (rtac conjI 1);
    1.13      by (Step_tac 1);
    1.14      by (Step_tac 1);
    1.15 -    be mp 1;
    1.16 -    br inf_lb1 1;
    1.17 +    by (etac mp 1);
    1.18 +    by (rtac inf_lb1 1);
    1.19      by (Step_tac 1);
    1.20      by (Step_tac 1);
    1.21 -    be mp 1;
    1.22 -    br inf_lb2 1;
    1.23 +    by (etac mp 1);
    1.24 +    by (rtac inf_lb2 1);
    1.25    (*==> (level 11)*)
    1.26 -    br (conjI RS (le_trans RS mp)) 1;
    1.27 -    br inf_lb2 2;
    1.28 +    by (rtac (conjI RS (le_trans RS mp)) 1);
    1.29 +    by (rtac inf_lb2 2);
    1.30      by (subgoal_tac "x && y = x" 1);
    1.31 -    be subst 1;
    1.32 +    by (etac subst 1);
    1.33      by (Fast_tac 1);
    1.34      by (stac inf_connect 1);
    1.35 -    ba 1;
    1.36 +    by (assume_tac 1);
    1.37  qed "mono_inf_eq";
    1.38  
    1.39  goalw thy [is_mono_def] "is_mono f = (ALL x y. f x || f y [= f (x || y))";
    1.40 -  by (safe_tac (claset()));
    1.41 +  by Safe_tac;
    1.42    (*==> (level 1)*)
    1.43      by (stac ge_sup_eq 1);
    1.44 -    br conjI 1;
    1.45 +    by (rtac conjI 1);
    1.46      by (Step_tac 1);
    1.47      by (Step_tac 1);
    1.48 -    be mp 1;
    1.49 -    br sup_ub1 1;
    1.50 +    by (etac mp 1);
    1.51 +    by (rtac sup_ub1 1);
    1.52      by (Step_tac 1);
    1.53      by (Step_tac 1);
    1.54 -    be mp 1;
    1.55 -    br sup_ub2 1;
    1.56 +    by (etac mp 1);
    1.57 +    by (rtac sup_ub2 1);
    1.58    (*==> (level 11)*)
    1.59 -    br (conjI RS (le_trans RS mp)) 1;
    1.60 -    br sup_ub1 1;
    1.61 +    by (rtac (conjI RS (le_trans RS mp)) 1);
    1.62 +    by (rtac sup_ub1 1);
    1.63      by (subgoal_tac "x || y = y" 1);
    1.64 -    be subst 1;
    1.65 +    by (etac subst 1);
    1.66      by (Fast_tac 1);
    1.67      by (stac sup_connect 1);
    1.68 -    ba 1;
    1.69 +    by (assume_tac 1);
    1.70  qed "mono_sup_eq";
    1.71  
    1.72