1.1 --- a/src/HOLCF/Cfun2.ML	Thu Sep 26 12:50:48 1996 +0200
     1.2 +++ b/src/HOLCF/Cfun2.ML	Thu Sep 26 15:14:23 1996 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  qed_goal "less_cfun" Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
     1.5  (fn prems =>
     1.6          [
     1.7 -        (rtac (inst_cfun_po RS ssubst) 1),
     1.8 +        (stac inst_cfun_po 1),
     1.9          (fold_goals_tac [less_cfun_def]),
    1.10          (rtac refl 1)
    1.11          ]);
    1.12 @@ -27,8 +27,8 @@
    1.13  qed_goalw "minimal_cfun" Cfun2.thy [UU_cfun_def] "UU_cfun << f"
    1.14  (fn prems =>
    1.15          [
    1.16 -        (rtac (less_cfun RS ssubst) 1),
    1.17 -        (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
    1.18 +        (stac less_cfun 1),
    1.19 +        (stac Abs_Cfun_inverse2 1),
    1.20          (rtac cont_const 1),
    1.21          (fold_goals_tac [UU_fun_def]),
    1.22          (rtac minimal_fun 1)
    1.23 @@ -112,10 +112,10 @@
    1.24  
    1.25  
    1.26  qed_goal "strictI" Cfun2.thy "f`x = UU ==> f`UU = UU" (fn prems => [
    1.27 -	cut_facts_tac prems 1,
    1.28 -	rtac (eq_UU_iff RS iffD2) 1,
    1.29 -	etac subst 1,
    1.30 -	rtac (minimal RS monofun_cfun_arg) 1]);
    1.31 +        cut_facts_tac prems 1,
    1.32 +        rtac (eq_UU_iff RS iffD2) 1,
    1.33 +        etac subst 1,
    1.34 +        rtac (minimal RS monofun_cfun_arg) 1]);
    1.35  
    1.36  
    1.37  (* ------------------------------------------------------------------------ *)
    1.38 @@ -184,7 +184,7 @@
    1.39          (etac lub_cfun_mono 1),
    1.40          (rtac contlubI 1),
    1.41          (strip_tac 1),
    1.42 -        (rtac (contlub_cfun_arg RS ext RS ssubst) 1),
    1.43 +        (stac (contlub_cfun_arg RS ext) 1),
    1.44          (atac 1),
    1.45          (etac ex_lubcfun 1),
    1.46          (atac 1)
    1.47 @@ -203,14 +203,14 @@
    1.48          (rtac conjI 1),
    1.49          (rtac ub_rangeI 1),  
    1.50          (rtac allI 1),
    1.51 -        (rtac (less_cfun RS ssubst) 1),
    1.52 -        (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
    1.53 +        (stac less_cfun 1),
    1.54 +        (stac Abs_Cfun_inverse2 1),
    1.55          (etac cont_lubcfun 1),
    1.56          (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
    1.57          (etac (monofun_fapp1 RS ch2ch_monofun) 1),
    1.58          (strip_tac 1),
    1.59 -        (rtac (less_cfun RS ssubst) 1),
    1.60 -        (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
    1.61 +        (stac less_cfun 1),
    1.62 +        (stac Abs_Cfun_inverse2 1),
    1.63          (etac cont_lubcfun 1),
    1.64          (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
    1.65          (etac (monofun_fapp1 RS ch2ch_monofun) 1),
    1.66 @@ -255,9 +255,9 @@
    1.67   (fn prems =>
    1.68          [
    1.69          (rtac (less_cfun RS iffD2) 1),
    1.70 -        (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
    1.71 +        (stac Abs_Cfun_inverse2 1),
    1.72          (resolve_tac prems 1),
    1.73 -        (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
    1.74 +        (stac Abs_Cfun_inverse2 1),
    1.75          (resolve_tac prems 1),
    1.76          (resolve_tac prems 1)
    1.77          ]);