Ran expandshort; used stac instead of ssubst
authorpaulson
Thu Sep 26 15:14:23 1996 +0200 (1996-09-26)
changeset 2033639de962ded4
parent 2032 1bbf1bdcaf56
child 2034 5079fdf938dd
Ran expandshort; used stac instead of ssubst
src/HOLCF/Cfun1.ML
src/HOLCF/Cfun2.ML
src/HOLCF/Cfun3.ML
src/HOLCF/Cont.ML
src/HOLCF/Cprod1.ML
src/HOLCF/Cprod2.ML
src/HOLCF/Cprod3.ML
src/HOLCF/Fix.ML
src/HOLCF/Fun1.ML
src/HOLCF/Fun2.ML
src/HOLCF/Holcfb.ML
src/HOLCF/Lift1.ML
src/HOLCF/Lift2.ML
src/HOLCF/Lift3.ML
src/HOLCF/Pcpo.ML
src/HOLCF/Porder.ML
src/HOLCF/ROOT.ML
src/HOLCF/Sprod0.ML
src/HOLCF/Sprod1.ML
src/HOLCF/Sprod2.ML
src/HOLCF/Sprod3.ML
src/HOLCF/Ssum2.ML
src/HOLCF/Ssum3.ML
src/HOLCF/Tr1.ML
src/HOLCF/Void.ML
src/HOLCF/ccc1.ML
src/HOLCF/domain/theorems.ML
src/HOLCF/ex/Hoare.ML
src/HOLCF/ex/Loop.ML
src/HOLCF/ex/loeckx.ML
src/HOLCF/explicit_domains/Coind.ML
src/HOLCF/explicit_domains/Dagstuhl.ML
src/HOLCF/explicit_domains/Dlist.ML
src/HOLCF/explicit_domains/Dnat.ML
src/HOLCF/explicit_domains/Dnat2.ML
src/HOLCF/explicit_domains/Stream.ML
src/HOLCF/explicit_domains/Stream2.ML
src/ZF/Arith.ML
src/ZF/Cardinal.ML
src/ZF/Cardinal_AC.ML
src/ZF/Epsilon.ML
src/ZF/Finite.ML
src/ZF/List.ML
src/ZF/Nat.ML
src/ZF/OrderType.ML
src/ZF/Ordinal.ML
src/ZF/Perm.ML
src/ZF/QUniv.ML
src/ZF/Univ.ML
src/ZF/WF.ML
src/ZF/add_ind_def.ML
src/ZF/cartprod.ML
src/ZF/domrange.ML
src/ZF/func.ML
src/ZF/indrule.ML
src/ZF/intr_elim.ML
     1.1 --- a/src/HOLCF/Cfun1.ML	Thu Sep 26 12:50:48 1996 +0200
     1.2 +++ b/src/HOLCF/Cfun1.ML	Thu Sep 26 15:14:23 1996 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  qed_goalw "CfunI" Cfun1.thy [Cfun_def] "(% x.x):Cfun"
     1.5   (fn prems =>
     1.6          [
     1.7 -        (rtac (mem_Collect_eq RS ssubst) 1),
     1.8 +        (stac mem_Collect_eq 1),
     1.9          (rtac cont_id 1)
    1.10          ]);
    1.11  
     2.1 --- a/src/HOLCF/Cfun2.ML	Thu Sep 26 12:50:48 1996 +0200
     2.2 +++ b/src/HOLCF/Cfun2.ML	Thu Sep 26 15:14:23 1996 +0200
     2.3 @@ -15,7 +15,7 @@
     2.4  qed_goal "less_cfun" Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
     2.5  (fn prems =>
     2.6          [
     2.7 -        (rtac (inst_cfun_po RS ssubst) 1),
     2.8 +        (stac inst_cfun_po 1),
     2.9          (fold_goals_tac [less_cfun_def]),
    2.10          (rtac refl 1)
    2.11          ]);
    2.12 @@ -27,8 +27,8 @@
    2.13  qed_goalw "minimal_cfun" Cfun2.thy [UU_cfun_def] "UU_cfun << f"
    2.14  (fn prems =>
    2.15          [
    2.16 -        (rtac (less_cfun RS ssubst) 1),
    2.17 -        (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
    2.18 +        (stac less_cfun 1),
    2.19 +        (stac Abs_Cfun_inverse2 1),
    2.20          (rtac cont_const 1),
    2.21          (fold_goals_tac [UU_fun_def]),
    2.22          (rtac minimal_fun 1)
    2.23 @@ -112,10 +112,10 @@
    2.24  
    2.25  
    2.26  qed_goal "strictI" Cfun2.thy "f`x = UU ==> f`UU = UU" (fn prems => [
    2.27 -	cut_facts_tac prems 1,
    2.28 -	rtac (eq_UU_iff RS iffD2) 1,
    2.29 -	etac subst 1,
    2.30 -	rtac (minimal RS monofun_cfun_arg) 1]);
    2.31 +        cut_facts_tac prems 1,
    2.32 +        rtac (eq_UU_iff RS iffD2) 1,
    2.33 +        etac subst 1,
    2.34 +        rtac (minimal RS monofun_cfun_arg) 1]);
    2.35  
    2.36  
    2.37  (* ------------------------------------------------------------------------ *)
    2.38 @@ -184,7 +184,7 @@
    2.39          (etac lub_cfun_mono 1),
    2.40          (rtac contlubI 1),
    2.41          (strip_tac 1),
    2.42 -        (rtac (contlub_cfun_arg RS ext RS ssubst) 1),
    2.43 +        (stac (contlub_cfun_arg RS ext) 1),
    2.44          (atac 1),
    2.45          (etac ex_lubcfun 1),
    2.46          (atac 1)
    2.47 @@ -203,14 +203,14 @@
    2.48          (rtac conjI 1),
    2.49          (rtac ub_rangeI 1),  
    2.50          (rtac allI 1),
    2.51 -        (rtac (less_cfun RS ssubst) 1),
    2.52 -        (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
    2.53 +        (stac less_cfun 1),
    2.54 +        (stac Abs_Cfun_inverse2 1),
    2.55          (etac cont_lubcfun 1),
    2.56          (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
    2.57          (etac (monofun_fapp1 RS ch2ch_monofun) 1),
    2.58          (strip_tac 1),
    2.59 -        (rtac (less_cfun RS ssubst) 1),
    2.60 -        (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
    2.61 +        (stac less_cfun 1),
    2.62 +        (stac Abs_Cfun_inverse2 1),
    2.63          (etac cont_lubcfun 1),
    2.64          (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
    2.65          (etac (monofun_fapp1 RS ch2ch_monofun) 1),
    2.66 @@ -255,9 +255,9 @@
    2.67   (fn prems =>
    2.68          [
    2.69          (rtac (less_cfun RS iffD2) 1),
    2.70 -        (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
    2.71 +        (stac Abs_Cfun_inverse2 1),
    2.72          (resolve_tac prems 1),
    2.73 -        (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
    2.74 +        (stac Abs_Cfun_inverse2 1),
    2.75          (resolve_tac prems 1),
    2.76          (resolve_tac prems 1)
    2.77          ]);
     3.1 --- a/src/HOLCF/Cfun3.ML	Thu Sep 26 12:50:48 1996 +0200
     3.2 +++ b/src/HOLCF/Cfun3.ML	Thu Sep 26 15:14:23 1996 +0200
     3.3 @@ -17,11 +17,11 @@
     3.4          (strip_tac 1),
     3.5          (rtac (expand_fun_eq RS iffD2) 1),
     3.6          (strip_tac 1),
     3.7 -        (rtac (thelub_cfun RS ssubst) 1),
     3.8 +        (stac thelub_cfun 1),
     3.9          (atac 1),
    3.10 -        (rtac (Cfunapp2 RS ssubst) 1),
    3.11 +        (stac Cfunapp2 1),
    3.12          (etac cont_lubcfun 1),
    3.13 -        (rtac (thelub_fun RS ssubst) 1),
    3.14 +        (stac thelub_fun 1),
    3.15          (etac (monofun_fapp1 RS ch2ch_monofun) 1),
    3.16          (rtac refl 1)
    3.17          ]);
    3.18 @@ -52,7 +52,7 @@
    3.19          (cut_facts_tac prems 1),
    3.20          (rtac trans 1),
    3.21          (etac (contlub_fapp1 RS contlubE RS spec RS mp RS fun_cong) 1),
    3.22 -        (rtac (thelub_fun RS ssubst) 1),
    3.23 +        (stac thelub_fun 1),
    3.24          (etac (monofun_fapp1 RS ch2ch_monofun) 1),
    3.25          (rtac refl 1)
    3.26          ]);
    3.27 @@ -137,12 +137,12 @@
    3.28          (cut_facts_tac prems 1),
    3.29          (rtac monofunI 1),
    3.30          (strip_tac 1),
    3.31 -        (rtac (less_cfun RS ssubst) 1),
    3.32 -        (rtac (less_fun RS ssubst) 1),
    3.33 +        (stac less_cfun 1),
    3.34 +        (stac less_fun 1),
    3.35          (rtac allI 1),
    3.36 -        (rtac (beta_cfun RS ssubst) 1),
    3.37 +        (stac beta_cfun 1),
    3.38          (etac spec 1),
    3.39 -        (rtac (beta_cfun RS ssubst) 1),
    3.40 +        (stac beta_cfun 1),
    3.41          (etac spec 1),
    3.42          (etac ((hd (tl prems)) RS spec RS monofunE RS spec RS spec RS mp) 1)
    3.43          ]);
    3.44 @@ -162,7 +162,7 @@
    3.45          (etac spec 1),
    3.46          (rtac contlubI 1),
    3.47          (strip_tac 1),
    3.48 -        (rtac (thelub_cfun RS ssubst) 1),
    3.49 +        (stac thelub_cfun 1),
    3.50          (rtac (cont2mono_LAM RS ch2ch_monofun) 1),
    3.51          (atac 1),
    3.52          (rtac (cont2mono RS allI) 1),
    3.53 @@ -170,7 +170,7 @@
    3.54          (atac 1),
    3.55          (res_inst_tac [("f","fabs")] arg_cong 1),
    3.56          (rtac ext 1),
    3.57 -        (rtac (beta_cfun RS ext RS ssubst) 1),
    3.58 +        (stac (beta_cfun RS ext) 1),
    3.59          (etac spec 1),
    3.60          (rtac (cont2contlub RS contlubE 
    3.61                  RS spec RS mp ) 1),
    3.62 @@ -208,9 +208,9 @@
    3.63  qed_goal "strict_fapp1" Cfun3.thy "(UU::'a->'b)`x = (UU::'b)"
    3.64   (fn prems =>
    3.65          [
    3.66 -        (rtac (inst_cfun_pcpo RS ssubst) 1),
    3.67 +        (stac inst_cfun_pcpo 1),
    3.68          (rewtac UU_cfun_def),
    3.69 -        (rtac (beta_cfun RS ssubst) 1),
    3.70 +        (stac beta_cfun 1),
    3.71          (cont_tac 1),
    3.72          (rtac refl 1)
    3.73          ]);
    3.74 @@ -243,15 +243,15 @@
    3.75          (rtac (less_fun RS iffD2) 1),
    3.76          (strip_tac 1),
    3.77          (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1),
    3.78 -        (rtac (Istrictify2 RS ssubst) 1),
    3.79 +        (stac Istrictify2 1),
    3.80          (atac 1),
    3.81 -        (rtac (Istrictify2 RS ssubst) 1),
    3.82 +        (stac Istrictify2 1),
    3.83          (atac 1),
    3.84          (rtac monofun_cfun_fun 1),
    3.85          (atac 1),
    3.86          (hyp_subst_tac 1),
    3.87 -        (rtac (Istrictify1 RS ssubst) 1),
    3.88 -        (rtac (Istrictify1 RS ssubst) 1),
    3.89 +        (stac Istrictify1 1),
    3.90 +        (stac Istrictify1 1),
    3.91          (rtac refl_less 1)
    3.92          ]);
    3.93  
    3.94 @@ -261,15 +261,15 @@
    3.95          (rtac monofunI 1),
    3.96          (strip_tac 1),
    3.97          (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
    3.98 -        (rtac (Istrictify2 RS ssubst) 1),
    3.99 +        (stac Istrictify2 1),
   3.100          (etac notUU_I 1),
   3.101          (atac 1),
   3.102 -        (rtac (Istrictify2 RS ssubst) 1),
   3.103 +        (stac Istrictify2 1),
   3.104          (atac 1),
   3.105          (rtac monofun_cfun_arg 1),
   3.106          (atac 1),
   3.107          (hyp_subst_tac 1),
   3.108 -        (rtac (Istrictify1 RS ssubst) 1),
   3.109 +        (stac Istrictify1 1),
   3.110          (rtac minimal 1)
   3.111          ]);
   3.112  
   3.113 @@ -281,22 +281,22 @@
   3.114          (strip_tac 1),
   3.115          (rtac (expand_fun_eq RS iffD2) 1),
   3.116          (strip_tac 1),
   3.117 -        (rtac (thelub_fun RS ssubst) 1),
   3.118 +        (stac thelub_fun 1),
   3.119          (etac (monofun_Istrictify1 RS ch2ch_monofun) 1),
   3.120          (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
   3.121 -        (rtac (Istrictify2 RS ssubst) 1),
   3.122 +        (stac Istrictify2 1),
   3.123          (atac 1),
   3.124 -        (rtac (Istrictify2 RS ext RS ssubst) 1),
   3.125 +        (stac (Istrictify2 RS ext) 1),
   3.126          (atac 1),
   3.127 -        (rtac (thelub_cfun RS ssubst) 1),
   3.128 +        (stac thelub_cfun 1),
   3.129          (atac 1),
   3.130 -        (rtac (beta_cfun RS ssubst) 1),
   3.131 +        (stac beta_cfun 1),
   3.132          (rtac cont_lubcfun 1),
   3.133          (atac 1),
   3.134          (rtac refl 1),
   3.135          (hyp_subst_tac 1),
   3.136 -        (rtac (Istrictify1 RS ssubst) 1),
   3.137 -        (rtac (Istrictify1 RS ext RS ssubst) 1),
   3.138 +        (stac Istrictify1 1),
   3.139 +        (stac (Istrictify1 RS ext) 1),
   3.140          (rtac (chain_UU_I_inverse RS sym) 1),
   3.141          (rtac (refl RS allI) 1)
   3.142          ]);
   3.143 @@ -310,7 +310,7 @@
   3.144          (res_inst_tac [("t","lub(range(Y))")] subst 1),
   3.145          (rtac sym 1),
   3.146          (atac 1),
   3.147 -        (rtac (Istrictify1 RS ssubst) 1),
   3.148 +        (stac Istrictify1 1),
   3.149          (rtac sym 1),
   3.150          (rtac chain_UU_I_inverse 1),
   3.151          (strip_tac 1),
   3.152 @@ -320,7 +320,7 @@
   3.153          (atac 1),
   3.154          (atac 1),
   3.155          (rtac Istrictify1 1),
   3.156 -        (rtac (Istrictify2 RS ssubst) 1),
   3.157 +        (stac Istrictify2 1),
   3.158          (atac 1),
   3.159          (res_inst_tac [("s","lub(range(%i. f`(Y i)))")] trans 1),
   3.160          (rtac contlub_cfun_arg 1),
   3.161 @@ -354,12 +354,12 @@
   3.162          "strictify`f`UU=UU"
   3.163   (fn prems =>
   3.164          [
   3.165 -        (rtac (beta_cfun RS ssubst) 1),
   3.166 +        (stac beta_cfun 1),
   3.167          (cont_tac 1),
   3.168          (rtac cont_Istrictify2 1),
   3.169          (rtac cont2cont_CF1L 1),
   3.170          (rtac cont_Istrictify1 1),
   3.171 -        (rtac (beta_cfun RS ssubst) 1),
   3.172 +        (stac beta_cfun 1),
   3.173          (rtac cont_Istrictify2 1),
   3.174          (rtac Istrictify1 1)
   3.175          ]);
   3.176 @@ -368,12 +368,12 @@
   3.177          "~x=UU ==> strictify`f`x=f`x"
   3.178   (fn prems =>
   3.179          [
   3.180 -        (rtac (beta_cfun RS ssubst) 1),
   3.181 +        (stac beta_cfun 1),
   3.182          (cont_tac 1),
   3.183          (rtac cont_Istrictify2 1),
   3.184          (rtac cont2cont_CF1L 1),
   3.185          (rtac cont_Istrictify1 1),
   3.186 -        (rtac (beta_cfun RS ssubst) 1),
   3.187 +        (stac beta_cfun 1),
   3.188          (rtac cont_Istrictify2 1),
   3.189          (rtac Istrictify2 1),
   3.190          (resolve_tac prems 1)
     4.1 --- a/src/HOLCF/Cont.ML	Thu Sep 26 12:50:48 1996 +0200
     4.2 +++ b/src/HOLCF/Cont.ML	Thu Sep 26 15:14:23 1996 +0200
     4.3 @@ -379,9 +379,9 @@
     4.4   (fn prems =>
     4.5          [
     4.6          (cut_facts_tac prems 1),
     4.7 -        (rtac ((hd prems) RS cont2contlub RS contlubE RS spec RS mp RS ssubst) 1),
     4.8 +        (stac ((hd prems) RS cont2contlub RS contlubE RS spec RS mp) 1),
     4.9          (atac 1),
    4.10 -        (rtac (thelub_fun RS ssubst) 1),
    4.11 +        (stac thelub_fun 1),
    4.12          (rtac ((hd prems) RS cont2mono RS ch2ch_monofun) 1),
    4.13          (atac 1),
    4.14          (rtac trans 1),
    4.15 @@ -456,7 +456,7 @@
    4.16          (rtac ((hd prems) RS cont2contlub RS 
    4.17                  contlubE RS spec RS mp RS ssubst) 1),
    4.18          (atac 1),
    4.19 -        (rtac (thelub_fun RS ssubst) 1),
    4.20 +        (stac thelub_fun 1),
    4.21          (rtac ch2ch_monofun 1),
    4.22          (etac cont2mono 1),
    4.23          (atac 1),
    4.24 @@ -489,7 +489,7 @@
    4.25          (rtac contlubI 1),
    4.26          (strip_tac 1),
    4.27          (rtac ext 1),
    4.28 -        (rtac (thelub_fun RS ssubst) 1),
    4.29 +        (stac thelub_fun 1),
    4.30          (rtac (cont2mono RS allI RS mono2mono_MF1L_rev RS ch2ch_monofun) 1),
    4.31          (etac spec 1),
    4.32          (atac 1),
     5.1 --- a/src/HOLCF/Cprod1.ML	Thu Sep 26 12:50:48 1996 +0200
     5.2 +++ b/src/HOLCF/Cprod1.ML	Thu Sep 26 15:14:23 1996 +0200
     5.3 @@ -80,7 +80,7 @@
     5.4          (dtac less_cprod2c 1),
     5.5          (etac conjE 1),
     5.6          (etac conjE 1),
     5.7 -        (rtac (Pair_eq RS ssubst) 1),
     5.8 +        (stac Pair_eq 1),
     5.9          (fast_tac (HOL_cs addSIs [antisym_less]) 1)
    5.10          ]);
    5.11  
    5.12 @@ -98,7 +98,7 @@
    5.13          (hyp_subst_tac 1),
    5.14          (dtac less_cprod2c 1),
    5.15          (dtac less_cprod2c 1),
    5.16 -        (rtac (less_cprod1b RS ssubst) 1),
    5.17 +        (stac less_cprod1b 1),
    5.18          (Simp_tac 1),
    5.19          (etac conjE 1),
    5.20          (etac conjE 1),
     6.1 --- a/src/HOLCF/Cprod2.ML	Thu Sep 26 12:50:48 1996 +0200
     6.2 +++ b/src/HOLCF/Cprod2.ML	Thu Sep 26 15:14:23 1996 +0200
     6.3 @@ -13,8 +13,8 @@
     6.4   (fn prems =>
     6.5          [
     6.6          (cut_facts_tac prems 1),
     6.7 -        (rtac (inst_cprod_po RS ssubst) 1),
     6.8 -        (rtac (less_cprod1b RS ssubst) 1),
     6.9 +        (stac inst_cprod_po 1),
    6.10 +        (stac less_cprod1b 1),
    6.11          (hyp_subst_tac 1),
    6.12          (Asm_simp_tac  1)
    6.13          ]);
    6.14 @@ -23,7 +23,7 @@
    6.15   "(p1 << p2) = (fst(p1)<<fst(p2) & snd(p1)<<snd(p2))"
    6.16   (fn prems =>
    6.17          [
    6.18 -        (rtac (inst_cprod_po RS ssubst) 1),
    6.19 +        (stac inst_cprod_po 1),
    6.20          (rtac less_cprod1b 1)
    6.21          ]);
    6.22  
     7.1 --- a/src/HOLCF/Cprod3.ML	Thu Sep 26 12:50:48 1996 +0200
     7.2 +++ b/src/HOLCF/Cprod3.ML	Thu Sep 26 15:14:23 1996 +0200
     7.3 @@ -40,7 +40,7 @@
     7.4          (strip_tac 1),
     7.5          (rtac (expand_fun_eq RS iffD2) 1),
     7.6          (strip_tac 1),
     7.7 -        (rtac (lub_fun RS thelubI RS ssubst) 1),
     7.8 +        (stac (lub_fun RS thelubI) 1),
     7.9          (etac (monofun_pair1 RS ch2ch_monofun) 1),
    7.10          (rtac trans 1),
    7.11          (rtac (thelub_cprod RS sym) 2),
    7.12 @@ -101,7 +101,7 @@
    7.13          [
    7.14          (rtac contlubI 1),
    7.15          (strip_tac 1),
    7.16 -        (rtac (lub_cprod RS thelubI RS ssubst) 1),
    7.17 +        (stac (lub_cprod RS thelubI) 1),
    7.18          (atac 1),
    7.19          (Simp_tac 1)
    7.20          ]);
    7.21 @@ -111,7 +111,7 @@
    7.22          [
    7.23          (rtac contlubI 1),
    7.24          (strip_tac 1),
    7.25 -        (rtac (lub_cprod RS thelubI RS ssubst) 1),
    7.26 +        (stac (lub_cprod RS thelubI) 1),
    7.27          (atac 1),
    7.28          (Simp_tac 1)
    7.29          ]);
    7.30 @@ -147,12 +147,12 @@
    7.31          "(LAM x y.(x,y))`a`b = (a,b)"
    7.32   (fn prems =>
    7.33          [
    7.34 -        (rtac (beta_cfun RS ssubst) 1),
    7.35 +        (stac beta_cfun 1),
    7.36          (cont_tac 1),
    7.37          (rtac cont_pair2 1),
    7.38          (rtac cont2cont_CF1L 1),
    7.39          (rtac cont_pair1 1),
    7.40 -        (rtac (beta_cfun RS ssubst) 1),
    7.41 +        (stac beta_cfun 1),
    7.42          (rtac cont_pair2 1),
    7.43          (rtac refl 1)
    7.44          ]);
    7.45 @@ -211,8 +211,8 @@
    7.46   (fn prems =>
    7.47          [
    7.48          (cut_facts_tac prems 1),
    7.49 -        (rtac (beta_cfun_cprod RS ssubst) 1),
    7.50 -        (rtac (beta_cfun RS ssubst) 1),
    7.51 +        (stac beta_cfun_cprod 1),
    7.52 +        (stac beta_cfun 1),
    7.53          (rtac cont_fst 1),
    7.54          (Simp_tac  1)
    7.55          ]);
    7.56 @@ -222,8 +222,8 @@
    7.57   (fn prems =>
    7.58          [
    7.59          (cut_facts_tac prems 1),
    7.60 -        (rtac (beta_cfun_cprod RS ssubst) 1),
    7.61 -        (rtac (beta_cfun RS ssubst) 1),
    7.62 +        (stac beta_cfun_cprod 1),
    7.63 +        (stac beta_cfun 1),
    7.64          (rtac cont_snd 1),
    7.65          (Simp_tac  1)
    7.66          ]);
    7.67 @@ -232,10 +232,10 @@
    7.68          [cfst_def,csnd_def,cpair_def] "<cfst`p , csnd`p> = p"
    7.69   (fn prems =>
    7.70          [
    7.71 -        (rtac (beta_cfun_cprod RS ssubst) 1),
    7.72 -        (rtac (beta_cfun RS ssubst) 1),
    7.73 +        (stac beta_cfun_cprod 1),
    7.74 +        (stac beta_cfun 1),
    7.75          (rtac cont_snd 1),
    7.76 -        (rtac (beta_cfun RS ssubst) 1),
    7.77 +        (stac beta_cfun 1),
    7.78          (rtac cont_fst 1),
    7.79          (rtac (surjective_pairing RS sym) 1)
    7.80          ]);
    7.81 @@ -245,13 +245,13 @@
    7.82   " (p1 << p2) = (cfst`p1 << cfst`p2 & csnd`p1 << csnd`p2)"
    7.83   (fn prems =>
    7.84          [
    7.85 -        (rtac (beta_cfun RS ssubst) 1),
    7.86 +        (stac beta_cfun 1),
    7.87          (rtac cont_snd 1),
    7.88 -        (rtac (beta_cfun RS ssubst) 1),
    7.89 +        (stac beta_cfun 1),
    7.90          (rtac cont_snd 1),
    7.91 -        (rtac (beta_cfun RS ssubst) 1),
    7.92 +        (stac beta_cfun 1),
    7.93          (rtac cont_fst 1),
    7.94 -        (rtac (beta_cfun RS ssubst) 1),
    7.95 +        (stac beta_cfun 1),
    7.96          (rtac cont_fst 1),
    7.97          (rtac less_cprod3b 1)
    7.98          ]);
    7.99 @@ -274,10 +274,10 @@
   7.100   (fn prems =>
   7.101          [
   7.102          (cut_facts_tac prems 1),
   7.103 -        (rtac (beta_cfun_cprod RS ssubst) 1),
   7.104 -        (rtac (beta_cfun RS ext RS ssubst) 1),
   7.105 +        (stac beta_cfun_cprod 1),
   7.106 +        (stac (beta_cfun RS ext) 1),
   7.107          (rtac cont_snd 1),
   7.108 -        (rtac (beta_cfun RS ext RS ssubst) 1),
   7.109 +        (stac (beta_cfun RS ext) 1),
   7.110          (rtac cont_fst 1),
   7.111          (rtac lub_cprod 1),
   7.112          (atac 1)
   7.113 @@ -293,7 +293,7 @@
   7.114          "csplit`f`<x,y> = f`x`y"
   7.115   (fn prems =>
   7.116          [
   7.117 -        (rtac (beta_cfun RS ssubst) 1),
   7.118 +        (stac beta_cfun 1),
   7.119          (cont_tacR 1),
   7.120          (Simp_tac 1),
   7.121          (simp_tac (!simpset addsimps [cfst2,csnd2]) 1)
   7.122 @@ -303,7 +303,7 @@
   7.123    "csplit`cpair`z=z"
   7.124   (fn prems =>
   7.125          [
   7.126 -        (rtac (beta_cfun RS ssubst) 1),
   7.127 +        (stac beta_cfun 1),
   7.128          (cont_tacR 1),
   7.129          (simp_tac (!simpset addsimps [surjective_pairing_Cprod2]) 1)
   7.130          ]);
     8.1 --- a/src/HOLCF/Fix.ML	Thu Sep 26 12:50:48 1996 +0200
     8.2 +++ b/src/HOLCF/Fix.ML	Thu Sep 26 15:14:23 1996 +0200
     8.3 @@ -31,10 +31,10 @@
     8.4          [
     8.5          (nat_ind_tac "n" 1),
     8.6          (Simp_tac 1),
     8.7 -	(rtac (iterate_Suc RS ssubst) 1),
     8.8 -	(rtac (iterate_Suc RS ssubst) 1),
     8.9 -	(etac ssubst 1),
    8.10 -	(rtac refl 1)
    8.11 +        (stac iterate_Suc 1),
    8.12 +        (stac iterate_Suc 1),
    8.13 +        (etac ssubst 1),
    8.14 +        (rtac refl 1)
    8.15          ]);
    8.16  
    8.17  (* ------------------------------------------------------------------------ *)
    8.18 @@ -74,7 +74,7 @@
    8.19  qed_goalw "Ifix_eq" Fix.thy  [Ifix_def] "Ifix F =F`(Ifix F)"
    8.20   (fn prems =>
    8.21          [
    8.22 -        (rtac (contlub_cfun_arg RS ssubst) 1),
    8.23 +        (stac contlub_cfun_arg 1),
    8.24          (rtac is_chain_iterate 1),
    8.25          (rtac antisym_less 1),
    8.26          (rtac lub_mono 1),
    8.27 @@ -146,7 +146,7 @@
    8.28          (rtac (lub_const RS thelubI RS sym) 1),
    8.29          (Asm_simp_tac 1),
    8.30          (rtac ext 1),
    8.31 -        (rtac (thelub_fun RS ssubst) 1),
    8.32 +        (stac thelub_fun 1),
    8.33          (rtac is_chainI 1),
    8.34          (rtac allI 1),
    8.35          (rtac (less_fun RS iffD2) 1),
    8.36 @@ -159,7 +159,7 @@
    8.37          (rtac ch2ch_fun 1),
    8.38          (rtac (monofun_iterate RS ch2ch_monofun) 1),
    8.39          (atac 1),
    8.40 -        (rtac (thelub_fun RS ssubst) 1),
    8.41 +        (stac thelub_fun 1),
    8.42          (rtac (monofun_iterate RS ch2ch_monofun) 1),
    8.43          (atac 1),
    8.44          (rtac contlub_cfun  1),
    8.45 @@ -266,7 +266,7 @@
    8.46          (rtac (monofun_iterate RS ch2ch_monofun) 1),
    8.47          (atac 1),
    8.48          (rtac fun_cong 1),
    8.49 -        (rtac (contlub_iterate RS contlubE RS spec RS mp RS ssubst) 1),
    8.50 +        (stac (contlub_iterate RS contlubE RS spec RS mp) 1),
    8.51          (atac 1),
    8.52          (rtac refl 1)
    8.53          ]);
    8.54 @@ -310,7 +310,7 @@
    8.55   (fn prems =>
    8.56          [
    8.57          (strip_tac 1),
    8.58 -        (rtac (contlub_Ifix_lemma1 RS ext RS ssubst) 1),
    8.59 +        (stac (contlub_Ifix_lemma1 RS ext) 1),
    8.60          (atac 1),
    8.61          (etac ex_lub_iterate 1)
    8.62          ]);
    8.63 @@ -488,15 +488,15 @@
    8.64   (fn prems =>
    8.65          [
    8.66          (cut_facts_tac prems 1),
    8.67 -        (rtac (fix_def2 RS ssubst) 1),
    8.68 +        (stac fix_def2 1),
    8.69          (rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
    8.70          (atac 1),
    8.71          (rtac is_chain_iterate 1),
    8.72          (rtac allI 1),
    8.73          (nat_ind_tac "i" 1),
    8.74 -        (rtac (iterate_0 RS ssubst) 1),
    8.75 +        (stac iterate_0 1),
    8.76          (atac 1),
    8.77 -        (rtac (iterate_Suc RS ssubst) 1),
    8.78 +        (stac iterate_Suc 1),
    8.79          (resolve_tac prems 1),
    8.80          (atac 1)
    8.81          ]);
    8.82 @@ -510,7 +510,7 @@
    8.83   (fn prems =>
    8.84          [
    8.85          (cut_facts_tac prems 1),
    8.86 -        (rtac (fix_def2 RS ssubst) 1),
    8.87 +        (stac fix_def2 1),
    8.88          (rtac (admw_def2 RS iffD1 RS spec RS mp) 1),
    8.89          (atac 1),
    8.90          (rtac allI 1),
    8.91 @@ -531,7 +531,7 @@
    8.92          (rtac mp 1),
    8.93          (etac spec 1),
    8.94          (atac 1),
    8.95 -        (rtac (lub_finch1 RS thelubI RS ssubst) 1),
    8.96 +        (stac (lub_finch1 RS thelubI) 1),
    8.97          (atac 1),
    8.98          (atac 1),
    8.99          (etac spec 1)
   8.100 @@ -598,9 +598,9 @@
   8.101          ]);
   8.102  
   8.103  qed_goalw "flat_eq" Fix.thy [is_flat_def] 
   8.104 -	"[| is_flat (x::'a); (a::'a) ~= UU |] ==> a << b = (a = b)" (fn prems=>[
   8.105 -	(cut_facts_tac prems 1),
   8.106 -	(fast_tac (HOL_cs addIs [refl_less]) 1)]);
   8.107 +        "[| is_flat (x::'a); (a::'a) ~= UU |] ==> a << b = (a = b)" (fn prems=>[
   8.108 +        (cut_facts_tac prems 1),
   8.109 +        (fast_tac (HOL_cs addIs [refl_less]) 1)]);
   8.110  
   8.111  (* ------------------------------------------------------------------------ *)
   8.112  (* lemmata for improved admissibility introdution rule                      *)
   8.113 @@ -611,35 +611,35 @@
   8.114  \  (!!Y. [| is_chain Y; !i. P (Y i); ~ finite_chain Y |] ==> P (lub (range Y)))\
   8.115  \ |] ==> P (lub (range Y))"
   8.116   (fn prems => [
   8.117 -	cut_facts_tac prems 1,
   8.118 -	case_tac "finite_chain Y" 1,
   8.119 -	 eresolve_tac prems 2, atac 2, atac 2,
   8.120 -	rewtac finite_chain_def,
   8.121 -	safe_tac HOL_cs,
   8.122 -	etac (lub_finch1 RS thelubI RS ssubst) 1, atac 1, etac spec 1]);
   8.123 +        cut_facts_tac prems 1,
   8.124 +        case_tac "finite_chain Y" 1,
   8.125 +         eresolve_tac prems 2, atac 2, atac 2,
   8.126 +        rewtac finite_chain_def,
   8.127 +        safe_tac HOL_cs,
   8.128 +        etac (lub_finch1 RS thelubI RS ssubst) 1, atac 1, etac spec 1]);
   8.129  
   8.130  qed_goal "increasing_chain_adm_lemma" Porder.thy 
   8.131  "[|is_chain Y; !i. P (Y i); \
   8.132  \  (!!Y. [| is_chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j|]\
   8.133  \ ==> P (lub (range Y))) |] ==> P (lub (range Y))"
   8.134   (fn prems => [
   8.135 -	cut_facts_tac prems 1,
   8.136 -	etac infinite_chain_adm_lemma 1, atac 1, etac thin_rl 1,
   8.137 -	rewtac finite_chain_def,
   8.138 -	safe_tac HOL_cs,
   8.139 -	etac swap 1,
   8.140 -	rewtac max_in_chain_def,
   8.141 -	resolve_tac prems 1, atac 1, atac 1,
   8.142 -	fast_tac (HOL_cs addDs [le_imp_less_or_eq] 
   8.143 -			 addEs [chain_mono RS mp]) 1]);
   8.144 +        cut_facts_tac prems 1,
   8.145 +        etac infinite_chain_adm_lemma 1, atac 1, etac thin_rl 1,
   8.146 +        rewtac finite_chain_def,
   8.147 +        safe_tac HOL_cs,
   8.148 +        etac swap 1,
   8.149 +        rewtac max_in_chain_def,
   8.150 +        resolve_tac prems 1, atac 1, atac 1,
   8.151 +        fast_tac (HOL_cs addDs [le_imp_less_or_eq] 
   8.152 +                         addEs [chain_mono RS mp]) 1]);
   8.153  
   8.154  qed_goalw "admI" Fix.thy [adm_def]
   8.155   "(!!Y. [| is_chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |]\
   8.156  \ ==> P(lub (range Y))) ==> adm P" 
   8.157   (fn prems => [
   8.158 -	strip_tac 1,
   8.159 -	etac increasing_chain_adm_lemma 1, atac 1,
   8.160 -	eresolve_tac prems 1, atac 1, atac 1]);
   8.161 +        strip_tac 1,
   8.162 +        etac increasing_chain_adm_lemma 1, atac 1,
   8.163 +        eresolve_tac prems 1, atac 1, atac 1]);
   8.164  
   8.165  
   8.166  (* ------------------------------------------------------------------------ *)
   8.167 @@ -881,7 +881,7 @@
   8.168          (cut_facts_tac prems 1),
   8.169          (rtac (adm_def2 RS iffD2) 1),
   8.170          (strip_tac 1),
   8.171 -        (rtac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1),
   8.172 +        (stac (cont2contlub RS contlubE RS spec RS mp) 1),
   8.173          (atac 1),
   8.174          (atac 1),
   8.175          (rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
   8.176 @@ -1000,7 +1000,7 @@
   8.177          (hyp_subst_tac 1),
   8.178          (Asm_simp_tac 1),
   8.179          (Asm_simp_tac 1),
   8.180 -	(asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1)
   8.181 +        (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1)
   8.182          ]);
   8.183  
   8.184    val adm_disj_lemma4 = prove_goal Fix.thy
   8.185 @@ -1012,14 +1012,14 @@
   8.186          (rtac allI 1),
   8.187          (res_inst_tac [("m","n"),("n","Suc(i)")] nat_less_cases 1),
   8.188          (res_inst_tac[("s","Y(Suc(i))"),
   8.189 -		      ("t","if n<Suc(i) then Y(Suc(i)) else Y n")] ssubst 1),
   8.190 +                      ("t","if n<Suc(i) then Y(Suc(i)) else Y n")] ssubst 1),
   8.191          (Asm_simp_tac 1),
   8.192          (etac allE 1),
   8.193          (rtac mp 1),
   8.194          (atac 1),
   8.195          (Asm_simp_tac 1),
   8.196          (res_inst_tac[("s","Y(n)"),
   8.197 -		      ("t","if n<Suc(i) then Y(Suc(i)) else Y(n)")] ssubst 1),
   8.198 +                      ("t","if n<Suc(i) then Y(Suc(i)) else Y(n)")] ssubst 1),
   8.199          (Asm_simp_tac 1),
   8.200          (hyp_subst_tac 1),
   8.201          (dtac spec 1),
   8.202 @@ -1027,7 +1027,7 @@
   8.203          (atac 1),
   8.204          (Asm_simp_tac 1),
   8.205          (res_inst_tac [("s","Y(n)"),
   8.206 -		       ("t","if n < Suc(i) then Y(Suc(i)) else Y(n)")]ssubst 1),
   8.207 +                       ("t","if n < Suc(i) then Y(Suc(i)) else Y(n)")]ssubst 1),
   8.208          (res_inst_tac [("s","False"),("t","n < Suc(i)")] ssubst 1),
   8.209          (rtac iffI 1),
   8.210          (etac FalseE 2),
   8.211 @@ -1061,7 +1061,7 @@
   8.212          (rtac (not_less_eq RS iffD2) 1),
   8.213          (atac 1),
   8.214          (atac 1),
   8.215 -        (rtac (if_False RS ssubst) 1),
   8.216 +        (stac if_False 1),
   8.217          (rtac refl 1)
   8.218          ]);
   8.219  
   8.220 @@ -1230,14 +1230,14 @@
   8.221  
   8.222  qed_goal "adm_not_conj"  Fix.thy  
   8.223  "[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))"(fn prems=>[
   8.224 -	cut_facts_tac prems 1,
   8.225 -	subgoal_tac 
   8.226 -	"(%x. ~ (P x & Q x)) = (%x. ~ P x | ~ Q x)" 1,
   8.227 -	rtac ext 2,
   8.228 -	fast_tac HOL_cs 2,
   8.229 -	etac ssubst 1,
   8.230 -	etac adm_disj 1,
   8.231 -	atac 1]);
   8.232 +        cut_facts_tac prems 1,
   8.233 +        subgoal_tac 
   8.234 +        "(%x. ~ (P x & Q x)) = (%x. ~ P x | ~ Q x)" 1,
   8.235 +        rtac ext 2,
   8.236 +        fast_tac HOL_cs 2,
   8.237 +        etac ssubst 1,
   8.238 +        etac adm_disj 1,
   8.239 +        atac 1]);
   8.240  
   8.241  val adm_thms = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
   8.242          adm_all2,adm_not_less,adm_not_free,adm_not_conj,adm_conj,adm_less];
     9.1 --- a/src/HOLCF/Fun1.ML	Thu Sep 26 12:50:48 1996 +0200
     9.2 +++ b/src/HOLCF/Fun1.ML	Thu Sep 26 15:14:23 1996 +0200
     9.3 @@ -23,7 +23,7 @@
     9.4  (fn prems =>
     9.5          [
     9.6          (cut_facts_tac prems 1),
     9.7 -        (rtac (expand_fun_eq RS ssubst) 1),
     9.8 +        (stac expand_fun_eq 1),
     9.9          (fast_tac (HOL_cs addSIs [antisym_less]) 1)
    9.10          ]);
    9.11  
    10.1 --- a/src/HOLCF/Fun2.ML	Thu Sep 26 12:50:48 1996 +0200
    10.2 +++ b/src/HOLCF/Fun2.ML	Thu Sep 26 15:14:23 1996 +0200
    10.3 @@ -15,7 +15,7 @@
    10.4  qed_goalw "minimal_fun"  Fun2.thy [UU_fun_def] "UU_fun << f"
    10.5  (fn prems =>
    10.6          [
    10.7 -        (rtac (inst_fun_po RS ssubst) 1),
    10.8 +        (stac inst_fun_po 1),
    10.9          (rewtac less_fun_def),
   10.10          (fast_tac (HOL_cs addSIs [minimal]) 1)
   10.11          ]);
   10.12 @@ -27,7 +27,7 @@
   10.13  qed_goal "less_fun"  Fun2.thy  "(f1 << f2) = (! x. f1(x) << f2(x))"
   10.14  (fn prems =>
   10.15          [
   10.16 -        (rtac (inst_fun_po RS ssubst) 1),
   10.17 +        (stac inst_fun_po 1),
   10.18          (fold_goals_tac [less_fun_def]),
   10.19          (rtac refl 1)
   10.20          ]);
   10.21 @@ -80,12 +80,12 @@
   10.22          (rtac conjI 1),
   10.23          (rtac ub_rangeI 1),
   10.24          (rtac allI 1),
   10.25 -        (rtac (less_fun RS ssubst) 1),
   10.26 +        (stac less_fun 1),
   10.27          (rtac allI 1),
   10.28          (rtac is_ub_thelub 1),
   10.29          (etac ch2ch_fun 1),
   10.30          (strip_tac 1),
   10.31 -        (rtac (less_fun RS ssubst) 1),
   10.32 +        (stac less_fun 1),
   10.33          (rtac allI 1),
   10.34          (rtac is_lub_thelub 1),
   10.35          (etac ch2ch_fun 1),
    11.1 --- a/src/HOLCF/Holcfb.ML	Thu Sep 26 12:50:48 1996 +0200
    11.2 +++ b/src/HOLCF/Holcfb.ML	Thu Sep 26 15:14:23 1996 +0200
    11.3 @@ -18,9 +18,9 @@
    11.4  (* val de_morgan2 = de_Morgan_conj RS sym;   "(~a | ~b)=(~(a & b))" *)
    11.5  
    11.6  
    11.7 -(* val notall2ex = not_all 		     "(~ (!x.P(x))) = (? x.~P(x))" *)
    11.8 +(* val notall2ex = not_all                   "(~ (!x.P(x))) = (? x.~P(x))" *)
    11.9  
   11.10 -(* val notex2all = not_ex		     "(~ (? x.P(x))) = (!x.~P(x))" *)
   11.11 +(* val notex2all = not_ex                    "(~ (? x.P(x))) = (!x.~P(x))" *)
   11.12  
   11.13  
   11.14  (* val selectI3 =  select_eq_Ex RS iffD2   "(? x. P(x)) ==> P(@ x.P(x))" *)
    12.1 --- a/src/HOLCF/Lift1.ML	Thu Sep 26 12:50:48 1996 +0200
    12.2 +++ b/src/HOLCF/Lift1.ML	Thu Sep 26 15:14:23 1996 +0200
    12.3 @@ -70,8 +70,8 @@
    12.4          "Ilift(f)(UU_lift)=UU"
    12.5   (fn prems =>
    12.6          [
    12.7 -        (rtac (Abs_Lift_inverse RS ssubst) 1),
    12.8 -        (rtac (sum_case_Inl RS ssubst) 1),
    12.9 +        (stac Abs_Lift_inverse 1),
   12.10 +        (stac sum_case_Inl 1),
   12.11          (rtac refl 1)
   12.12          ]);
   12.13  
   12.14 @@ -79,8 +79,8 @@
   12.15          "Ilift(f)(Iup(x))=f`x"
   12.16   (fn prems =>
   12.17          [
   12.18 -        (rtac (Abs_Lift_inverse RS ssubst) 1),
   12.19 -        (rtac (sum_case_Inr RS ssubst) 1),
   12.20 +        (stac Abs_Lift_inverse 1),
   12.21 +        (stac sum_case_Inr 1),
   12.22          (rtac refl 1)
   12.23          ]);
   12.24  
   12.25 @@ -90,8 +90,8 @@
   12.26          "less_lift(UU_lift)(z)"
   12.27   (fn prems =>
   12.28          [
   12.29 -        (rtac (Abs_Lift_inverse RS ssubst) 1),
   12.30 -        (rtac (sum_case_Inl RS ssubst) 1),
   12.31 +        (stac Abs_Lift_inverse 1),
   12.32 +        (stac sum_case_Inl 1),
   12.33          (rtac TrueI 1)
   12.34          ]);
   12.35  
   12.36 @@ -102,10 +102,10 @@
   12.37          (rtac notI 1),
   12.38          (rtac iffD1 1),
   12.39          (atac 2),
   12.40 -        (rtac (Abs_Lift_inverse RS ssubst) 1),
   12.41 -        (rtac (Abs_Lift_inverse RS ssubst) 1),
   12.42 -        (rtac (sum_case_Inr RS ssubst) 1),
   12.43 -        (rtac (sum_case_Inl RS ssubst) 1),
   12.44 +        (stac Abs_Lift_inverse 1),
   12.45 +        (stac Abs_Lift_inverse 1),
   12.46 +        (stac sum_case_Inr 1),
   12.47 +        (stac sum_case_Inl 1),
   12.48          (rtac refl 1)
   12.49          ]);
   12.50  
   12.51 @@ -113,10 +113,10 @@
   12.52          "less_lift (Iup x) (Iup y)=(x<<y)"
   12.53   (fn prems =>
   12.54          [
   12.55 -        (rtac (Abs_Lift_inverse RS ssubst) 1),
   12.56 -        (rtac (Abs_Lift_inverse RS ssubst) 1),
   12.57 -        (rtac (sum_case_Inr RS ssubst) 1),
   12.58 -        (rtac (sum_case_Inr RS ssubst) 1),
   12.59 +        (stac Abs_Lift_inverse 1),
   12.60 +        (stac Abs_Lift_inverse 1),
   12.61 +        (stac sum_case_Inr 1),
   12.62 +        (stac sum_case_Inr 1),
   12.63          (rtac refl 1)
   12.64          ]);
   12.65  
    13.1 --- a/src/HOLCF/Lift2.ML	Thu Sep 26 12:50:48 1996 +0200
    13.2 +++ b/src/HOLCF/Lift2.ML	Thu Sep 26 15:14:23 1996 +0200
    13.3 @@ -15,7 +15,7 @@
    13.4  qed_goal "minimal_lift" Lift2.thy "UU_lift << z"
    13.5   (fn prems =>
    13.6          [
    13.7 -        (rtac (inst_lift_po RS ssubst) 1),
    13.8 +        (stac inst_lift_po 1),
    13.9          (rtac less_lift1a 1)
   13.10          ]);
   13.11  
   13.12 @@ -26,14 +26,14 @@
   13.13  qed_goal "less_lift2b" Lift2.thy "~ Iup(x) << UU_lift"
   13.14   (fn prems =>
   13.15          [
   13.16 -        (rtac (inst_lift_po RS ssubst) 1),
   13.17 +        (stac inst_lift_po 1),
   13.18          (rtac less_lift1b 1)
   13.19          ]);
   13.20  
   13.21  qed_goal "less_lift2c" Lift2.thy "(Iup(x)<<Iup(y)) = (x<<y)"
   13.22   (fn prems =>
   13.23          [
   13.24 -        (rtac (inst_lift_po RS ssubst) 1),
   13.25 +        (stac inst_lift_po 1),
   13.26          (rtac less_lift1c 1)
   13.27          ]);
   13.28  
    14.1 --- a/src/HOLCF/Lift3.ML	Thu Sep 26 12:50:48 1996 +0200
    14.2 +++ b/src/HOLCF/Lift3.ML	Thu Sep 26 15:14:23 1996 +0200
    14.3 @@ -15,14 +15,14 @@
    14.4  qed_goal "less_lift3b" Lift3.thy "~ Iup(x) << UU"
    14.5   (fn prems =>
    14.6          [
    14.7 -        (rtac (inst_lift_pcpo RS ssubst) 1),
    14.8 +        (stac inst_lift_pcpo 1),
    14.9          (rtac less_lift2b 1)
   14.10          ]);
   14.11  
   14.12  qed_goal "defined_Iup2" Lift3.thy "Iup(x) ~= UU"
   14.13   (fn prems =>
   14.14          [
   14.15 -        (rtac (inst_lift_pcpo RS ssubst) 1),
   14.16 +        (stac inst_lift_pcpo 1),
   14.17          (rtac defined_Iup 1)
   14.18          ]);
   14.19  
   14.20 @@ -83,11 +83,11 @@
   14.21          (rtac contlubI 1),
   14.22          (strip_tac 1),
   14.23          (rtac disjE 1),
   14.24 -        (rtac (thelub_lift1a RS ssubst) 2),
   14.25 +        (stac thelub_lift1a 2),
   14.26          (atac 2),
   14.27          (atac 2),
   14.28          (asm_simp_tac Lift0_ss 2),
   14.29 -        (rtac (thelub_lift1b RS ssubst) 3),
   14.30 +        (stac thelub_lift1b 3),
   14.31          (atac 3),
   14.32          (atac 3),
   14.33          (fast_tac HOL_cs 1),
   14.34 @@ -100,7 +100,7 @@
   14.35          (dtac spec 2),
   14.36          (etac spec 2),
   14.37          (atac 2),
   14.38 -        (rtac (contlub_cfun_arg RS ssubst) 1),
   14.39 +        (stac contlub_cfun_arg 1),
   14.40          (etac (monofun_Ilift2 RS ch2ch_monofun) 1),
   14.41          (rtac lub_equal2 1),
   14.42          (rtac (monofun_fapp2 RS ch2ch_monofun) 2),
   14.43 @@ -120,7 +120,7 @@
   14.44          (asm_simp_tac Lift0_ss 2),
   14.45          (res_inst_tac [("P","Y(i) = UU")] notE 1),
   14.46          (fast_tac HOL_cs 1),
   14.47 -        (rtac (inst_lift_pcpo RS ssubst) 1),
   14.48 +        (stac inst_lift_pcpo 1),
   14.49          (atac 1)
   14.50          ]);
   14.51  
   14.52 @@ -149,7 +149,7 @@
   14.53   (fn prems =>
   14.54          [
   14.55          (simp_tac (Lift0_ss addsimps [cont_Iup]) 1),
   14.56 -        (rtac (inst_lift_pcpo RS ssubst) 1),
   14.57 +        (stac inst_lift_pcpo 1),
   14.58          (rtac Exh_Lift 1)
   14.59          ]);
   14.60  
   14.61 @@ -185,11 +185,11 @@
   14.62  qed_goalw "lift1" Lift3.thy [up_def,lift_def] "lift`f`UU=UU"
   14.63   (fn prems =>
   14.64          [
   14.65 -        (rtac (inst_lift_pcpo RS ssubst) 1),
   14.66 -        (rtac (beta_cfun RS ssubst) 1),
   14.67 +        (stac inst_lift_pcpo 1),
   14.68 +        (stac beta_cfun 1),
   14.69          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
   14.70                  cont_Ilift2,cont2cont_CF1L]) 1)),
   14.71 -        (rtac (beta_cfun RS ssubst) 1),
   14.72 +        (stac beta_cfun 1),
   14.73          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
   14.74                  cont_Ilift2,cont2cont_CF1L]) 1)),
   14.75          (simp_tac (Lift0_ss addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
   14.76 @@ -198,12 +198,12 @@
   14.77  qed_goalw "lift2" Lift3.thy [up_def,lift_def] "lift`f`(up`x)=f`x"
   14.78   (fn prems =>
   14.79          [
   14.80 -        (rtac (beta_cfun RS ssubst) 1),
   14.81 +        (stac beta_cfun 1),
   14.82          (rtac cont_Iup 1),
   14.83 -        (rtac (beta_cfun RS ssubst) 1),
   14.84 +        (stac beta_cfun 1),
   14.85          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
   14.86                  cont_Ilift2,cont2cont_CF1L]) 1)),
   14.87 -        (rtac (beta_cfun RS ssubst) 1),
   14.88 +        (stac beta_cfun 1),
   14.89          (rtac cont_Ilift2 1),
   14.90          (simp_tac (Lift0_ss addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
   14.91          ]);
   14.92 @@ -229,14 +229,14 @@
   14.93   (fn prems =>
   14.94          [
   14.95          (cut_facts_tac prems 1),
   14.96 -        (rtac (beta_cfun RS ssubst) 1),
   14.97 +        (stac beta_cfun 1),
   14.98          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
   14.99                  cont_Ilift2,cont2cont_CF1L]) 1)),
  14.100 -        (rtac (beta_cfun RS ssubst) 1),
  14.101 +        (stac beta_cfun 1),
  14.102          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
  14.103                  cont_Ilift2,cont2cont_CF1L]) 1)),
  14.104  
  14.105 -        (rtac (beta_cfun RS ext RS ssubst) 1),
  14.106 +        (stac (beta_cfun RS ext) 1),
  14.107          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
  14.108                  cont_Ilift2,cont2cont_CF1L]) 1)),
  14.109          (rtac thelub_lift1a 1),
  14.110 @@ -257,7 +257,7 @@
  14.111   (fn prems =>
  14.112          [
  14.113          (cut_facts_tac prems 1),
  14.114 -        (rtac (inst_lift_pcpo RS ssubst) 1),
  14.115 +        (stac inst_lift_pcpo 1),
  14.116          (rtac thelub_lift1b 1),
  14.117          (atac 1),
  14.118          (strip_tac 1),
    15.1 --- a/src/HOLCF/Pcpo.ML	Thu Sep 26 12:50:48 1996 +0200
    15.2 +++ b/src/HOLCF/Pcpo.ML	Thu Sep 26 15:14:23 1996 +0200
    15.3 @@ -162,7 +162,7 @@
    15.4  qed_goal "UU_I" Pcpo.thy "x << UU ==> x = UU"
    15.5   (fn prems =>
    15.6          [
    15.7 -        (rtac (eq_UU_iff RS ssubst) 1),
    15.8 +        (stac eq_UU_iff 1),
    15.9          (resolve_tac prems 1)
   15.10          ]);
   15.11  
   15.12 @@ -251,7 +251,7 @@
   15.13  qed_goal "unique_void2" Pcpo.thy "(x::void)=UU"
   15.14   (fn prems =>
   15.15          [
   15.16 -        (rtac (inst_void_pcpo RS ssubst) 1),
   15.17 +        (stac inst_void_pcpo 1),
   15.18          (rtac (Rep_Void_inverse RS subst) 1),
   15.19          (rtac (Rep_Void_inverse RS subst) 1),
   15.20          (rtac arg_cong 1),
    16.1 --- a/src/HOLCF/Porder.ML	Thu Sep 26 12:50:48 1996 +0200
    16.2 +++ b/src/HOLCF/Porder.ML	Thu Sep 26 15:14:23 1996 +0200
    16.3 @@ -62,7 +62,7 @@
    16.4          (nat_ind_tac "y" 1),
    16.5          (rtac impI 1),
    16.6          (etac less_zeroE 1),
    16.7 -        (rtac (less_Suc_eq RS ssubst) 1),
    16.8 +        (stac less_Suc_eq 1),
    16.9          (strip_tac 1),
   16.10          (etac disjE 1),
   16.11          (rtac trans_less 1),
   16.12 @@ -108,7 +108,7 @@
   16.13  (fn prems =>
   16.14          [
   16.15          (cut_facts_tac prems 1),
   16.16 -        (rtac (lub RS ssubst) 1),
   16.17 +        (stac lub 1),
   16.18          (etac (select_eq_Ex RS iffD2) 1)
   16.19          ]);
   16.20  
   16.21 @@ -123,7 +123,7 @@
   16.22          "(? x. M <<| x)  = M <<| lub(M)"
   16.23  (fn prems => 
   16.24          [
   16.25 -        (rtac (lub RS ssubst) 1),
   16.26 +        (stac lub 1),
   16.27          (rtac (select_eq_Ex RS subst) 1),
   16.28          (rtac refl 1)
   16.29          ]);
   16.30 @@ -134,7 +134,7 @@
   16.31          [
   16.32          (cut_facts_tac prems 1), 
   16.33          (rtac unique_lub 1),
   16.34 -        (rtac (lub RS ssubst) 1),
   16.35 +        (stac lub 1),
   16.36          (etac selectI 1),
   16.37          (atac 1)
   16.38          ]);
   16.39 @@ -217,7 +217,7 @@
   16.40  qed_goal "less_void" Porder.thy "((u1::void) << u2) = (u1 = u2)"
   16.41  (fn prems =>
   16.42          [
   16.43 -        (rtac (inst_void_po RS ssubst) 1),
   16.44 +        (stac inst_void_po 1),
   16.45          (rewtac less_void_def),
   16.46          (rtac iffI 1),
   16.47          (rtac injD 1),
   16.48 @@ -234,7 +234,7 @@
   16.49  qed_goal "minimal_void" Porder.thy      "UU_void << x"
   16.50  (fn prems =>
   16.51          [
   16.52 -        (rtac (inst_void_po RS ssubst) 1),
   16.53 +        (stac inst_void_po 1),
   16.54          (rewtac less_void_def),
   16.55          (simp_tac (!simpset addsimps [unique_void]) 1)
   16.56          ]);
   16.57 @@ -249,7 +249,7 @@
   16.58          (rtac conjI 1),
   16.59          (rewtac is_ub),
   16.60          (strip_tac 1),
   16.61 -        (rtac (inst_void_po RS ssubst) 1),
   16.62 +        (stac inst_void_po 1),
   16.63          (rewtac less_void_def),
   16.64          (simp_tac (!simpset addsimps [unique_void]) 1),
   16.65          (strip_tac 1),
    17.1 --- a/src/HOLCF/ROOT.ML	Thu Sep 26 12:50:48 1996 +0200
    17.2 +++ b/src/HOLCF/ROOT.ML	Thu Sep 26 15:14:23 1996 +0200
    17.3 @@ -12,7 +12,7 @@
    17.4  
    17.5  (* start 8bit 1 *)
    17.6  val banner = 
    17.7 -	"HOLCF with sections axioms,ops,domain,generated and 8bit characters";
    17.8 +        "HOLCF with sections axioms,ops,domain,generated and 8bit characters";
    17.9  (* end 8bit 1 *)
   17.10  
   17.11  writeln banner;
    18.1 --- a/src/HOLCF/Sprod0.ML	Thu Sep 26 12:50:48 1996 +0200
    18.2 +++ b/src/HOLCF/Sprod0.ML	Thu Sep 26 15:14:23 1996 +0200
    18.3 @@ -225,7 +225,7 @@
    18.4          "Isfst(Ispair UU y) = UU"
    18.5  (fn prems =>
    18.6          [
    18.7 -        (rtac (strict_Ispair1 RS ssubst) 1),
    18.8 +        (stac strict_Ispair1 1),
    18.9          (rtac strict_Isfst 1),
   18.10          (rtac refl 1)
   18.11          ]);
   18.12 @@ -234,7 +234,7 @@
   18.13          "Isfst(Ispair x UU) = UU"
   18.14  (fn prems =>
   18.15          [
   18.16 -        (rtac (strict_Ispair2 RS ssubst) 1),
   18.17 +        (stac strict_Ispair2 1),
   18.18          (rtac strict_Isfst 1),
   18.19          (rtac refl 1)
   18.20          ]);
   18.21 @@ -259,7 +259,7 @@
   18.22          "Issnd(Ispair UU y) = UU"
   18.23  (fn prems =>
   18.24          [
   18.25 -        (rtac (strict_Ispair1 RS ssubst) 1),
   18.26 +        (stac strict_Ispair1 1),
   18.27          (rtac strict_Issnd 1),
   18.28          (rtac refl 1)
   18.29          ]);
   18.30 @@ -268,7 +268,7 @@
   18.31          "Issnd(Ispair x UU) = UU"
   18.32  (fn prems =>
   18.33          [
   18.34 -        (rtac (strict_Ispair2 RS ssubst) 1),
   18.35 +        (stac strict_Ispair2 1),
   18.36          (rtac strict_Issnd 1),
   18.37          (rtac refl 1)
   18.38          ]);
    19.1 --- a/src/HOLCF/Sprod1.ML	Thu Sep 26 12:50:48 1996 +0200
    19.2 +++ b/src/HOLCF/Sprod1.ML	Thu Sep 26 15:14:23 1996 +0200
    19.3 @@ -96,7 +96,7 @@
    19.4          (res_inst_tac [("p","p")] IsprodE 1),
    19.5          (etac less_sprod1a 1),
    19.6          (hyp_subst_tac 1),
    19.7 -        (rtac (less_sprod1b RS ssubst) 1),
    19.8 +        (stac less_sprod1b 1),
    19.9          (rtac defined_Ispair 1),
   19.10          (REPEAT (fast_tac (HOL_cs addIs [refl_less]) 1))
   19.11          ]);
   19.12 @@ -146,7 +146,7 @@
   19.13          (hyp_subst_tac 1),
   19.14          (res_inst_tac [("Q","p2=Ispair(UU::'a)(UU::'b)")]
   19.15                   (excluded_middle RS disjE) 1),
   19.16 -        (rtac (defined_Ispair RS less_sprod1b RS ssubst) 1),
   19.17 +        (stac (defined_Ispair RS less_sprod1b) 1),
   19.18          (REPEAT (atac 1)),
   19.19          (rtac conjI 1),
   19.20          (res_inst_tac [("y","Isfst(p2)")] trans_less 1),
    20.1 --- a/src/HOLCF/Sprod2.ML	Thu Sep 26 12:50:48 1996 +0200
    20.2 +++ b/src/HOLCF/Sprod2.ML	Thu Sep 26 15:14:23 1996 +0200
    20.3 @@ -18,7 +18,7 @@
    20.4  (fn prems =>
    20.5          [
    20.6          (cut_facts_tac prems 1),
    20.7 -        (rtac (inst_sprod_po RS ssubst) 1),
    20.8 +        (stac inst_sprod_po 1),
    20.9          (etac less_sprod1a 1)
   20.10          ]);
   20.11  
   20.12 @@ -29,7 +29,7 @@
   20.13  (fn prems =>
   20.14          [
   20.15          (cut_facts_tac prems 1),
   20.16 -        (rtac (inst_sprod_po RS ssubst) 1),
   20.17 +        (stac inst_sprod_po 1),
   20.18          (etac less_sprod1b 1)
   20.19          ]);
   20.20  
   20.21 @@ -84,17 +84,17 @@
   20.22          (rtac (less_sprod3b RS iffD2) 1),
   20.23          (atac 1),
   20.24          (rtac conjI 1),
   20.25 -        (rtac (Isfst RS ssubst) 1),
   20.26 +        (stac Isfst 1),
   20.27          (etac (strict_Ispair_rev RS conjunct1) 1),
   20.28          (etac (strict_Ispair_rev RS conjunct2) 1),
   20.29 -        (rtac (Isfst RS ssubst) 1),
   20.30 +        (stac Isfst 1),
   20.31          (etac (strict_Ispair_rev RS conjunct1) 1),
   20.32          (etac (strict_Ispair_rev RS conjunct2) 1),
   20.33          (atac 1),
   20.34 -        (rtac (Issnd RS ssubst) 1),
   20.35 +        (stac Issnd 1),
   20.36          (etac (strict_Ispair_rev RS conjunct1) 1),
   20.37          (etac (strict_Ispair_rev RS conjunct2) 1),
   20.38 -        (rtac (Issnd RS ssubst) 1),
   20.39 +        (stac Issnd 1),
   20.40          (etac (strict_Ispair_rev RS conjunct1) 1),
   20.41          (etac (strict_Ispair_rev RS conjunct2) 1),
   20.42          (rtac refl_less 1),
   20.43 @@ -122,17 +122,17 @@
   20.44          (rtac (less_sprod3b RS iffD2) 1),
   20.45          (atac 1),
   20.46          (rtac conjI 1),
   20.47 -        (rtac (Isfst RS ssubst) 1),
   20.48 +        (stac Isfst 1),
   20.49          (etac (strict_Ispair_rev RS conjunct1) 1),
   20.50          (etac (strict_Ispair_rev RS conjunct2) 1),
   20.51 -        (rtac (Isfst RS ssubst) 1),
   20.52 +        (stac Isfst 1),
   20.53          (etac (strict_Ispair_rev RS conjunct1) 1),
   20.54          (etac (strict_Ispair_rev RS conjunct2) 1),
   20.55          (rtac refl_less 1),
   20.56 -        (rtac (Issnd RS ssubst) 1),
   20.57 +        (stac Issnd 1),
   20.58          (etac (strict_Ispair_rev RS conjunct1) 1),
   20.59          (etac (strict_Ispair_rev RS conjunct2) 1),
   20.60 -        (rtac (Issnd RS ssubst) 1),
   20.61 +        (stac Issnd 1),
   20.62          (etac (strict_Ispair_rev RS conjunct1) 1),
   20.63          (etac (strict_Ispair_rev RS conjunct2) 1),
   20.64          (atac 1),
   20.65 @@ -174,7 +174,7 @@
   20.66          (hyp_subst_tac 1),
   20.67          (rtac trans_less 1),
   20.68          (rtac minimal 2),
   20.69 -        (rtac (strict_Isfst1 RS ssubst) 1),
   20.70 +        (stac strict_Isfst1 1),
   20.71          (rtac refl_less 1),
   20.72          (hyp_subst_tac 1),
   20.73          (res_inst_tac [("p","y")] IsprodE 1),
   20.74 @@ -183,10 +183,10 @@
   20.75          (rtac refl_less 2),
   20.76          (etac (less_sprod4b RS sym RS arg_cong) 1),
   20.77          (hyp_subst_tac 1),
   20.78 -        (rtac (Isfst RS ssubst) 1),
   20.79 +        (stac Isfst 1),
   20.80          (atac 1),
   20.81          (atac 1),
   20.82 -        (rtac (Isfst RS ssubst) 1),
   20.83 +        (stac Isfst 1),
   20.84          (atac 1),
   20.85          (atac 1),
   20.86          (etac (less_sprod4c RS  conjunct1) 1),
   20.87 @@ -201,7 +201,7 @@
   20.88          (hyp_subst_tac 1),
   20.89          (rtac trans_less 1),
   20.90          (rtac minimal 2),
   20.91 -        (rtac (strict_Issnd1 RS ssubst) 1),
   20.92 +        (stac strict_Issnd1 1),
   20.93          (rtac refl_less 1),
   20.94          (hyp_subst_tac 1),
   20.95          (res_inst_tac [("p","y")] IsprodE 1),
   20.96 @@ -210,10 +210,10 @@
   20.97          (rtac refl_less 2),
   20.98          (etac (less_sprod4b RS sym RS arg_cong) 1),
   20.99          (hyp_subst_tac 1),
  20.100 -        (rtac (Issnd RS ssubst) 1),
  20.101 +        (stac Issnd 1),
  20.102          (atac 1),
  20.103          (atac 1),
  20.104 -        (rtac (Issnd RS ssubst) 1),
  20.105 +        (stac Issnd 1),
  20.106          (atac 1),
  20.107          (atac 1),
  20.108          (etac (less_sprod4c RS  conjunct2) 1),
    21.1 --- a/src/HOLCF/Sprod3.ML	Thu Sep 26 12:50:48 1996 +0200
    21.2 +++ b/src/HOLCF/Sprod3.ML	Thu Sep 26 15:14:23 1996 +0200
    21.3 @@ -98,7 +98,7 @@
    21.4          (strip_tac 1),
    21.5          (rtac (expand_fun_eq RS iffD2) 1),
    21.6          (strip_tac 1),
    21.7 -        (rtac (lub_fun RS thelubI RS ssubst) 1),
    21.8 +        (stac (lub_fun RS thelubI) 1),
    21.9          (etac (monofun_Ispair1 RS ch2ch_monofun) 1),
   21.10          (rtac trans 1),
   21.11          (rtac (thelub_sprod RS sym) 2),
   21.12 @@ -237,7 +237,7 @@
   21.13          [
   21.14          (rtac contlubI 1),
   21.15          (strip_tac 1),
   21.16 -        (rtac (lub_sprod RS thelubI RS ssubst) 1),
   21.17 +        (stac (lub_sprod RS thelubI) 1),
   21.18          (atac 1),
   21.19          (res_inst_tac [("Q","lub(range(%i. Issnd(Y(i))))=UU")]  
   21.20                  (excluded_middle RS disjE) 1),
   21.21 @@ -253,16 +253,16 @@
   21.22          (rtac strict_Isfst 1),
   21.23          (rtac swap 1),
   21.24          (etac (defined_IsfstIssnd RS conjunct2) 2),
   21.25 -	(fast_tac (HOL_cs addSDs [monofun_Issnd RS ch2ch_monofun RS 
   21.26 -				  chain_UU_I RS spec]) 1)
   21.27 -	]);
   21.28 +        (fast_tac (HOL_cs addSDs [monofun_Issnd RS ch2ch_monofun RS 
   21.29 +                                  chain_UU_I RS spec]) 1)
   21.30 +        ]);
   21.31  
   21.32  qed_goal "contlub_Issnd" Sprod3.thy "contlub(Issnd)"
   21.33  (fn prems =>
   21.34          [
   21.35          (rtac contlubI 1),
   21.36          (strip_tac 1),
   21.37 -        (rtac (lub_sprod RS thelubI RS ssubst) 1),
   21.38 +        (stac (lub_sprod RS thelubI) 1),
   21.39          (atac 1),
   21.40          (res_inst_tac [("Q","lub(range(%i. Isfst(Y(i))))=UU")]
   21.41           (excluded_middle RS disjE) 1),
   21.42 @@ -278,8 +278,8 @@
   21.43          (rtac swap 1),
   21.44          (etac (defined_IsfstIssnd RS conjunct1) 2),
   21.45          (fast_tac (HOL_cs addSDs [monofun_Isfst RS ch2ch_monofun RS
   21.46 -				  chain_UU_I RS spec]) 1)
   21.47 -	]);
   21.48 +                                  chain_UU_I RS spec]) 1)
   21.49 +        ]);
   21.50  
   21.51  qed_goal "cont_Isfst" Sprod3.thy "cont(Isfst)"
   21.52  (fn prems =>
   21.53 @@ -319,12 +319,12 @@
   21.54          "(LAM x y.Ispair x y)`a`b = Ispair a b"
   21.55   (fn prems =>
   21.56          [
   21.57 -        (rtac (beta_cfun RS ssubst) 1),
   21.58 +        (stac beta_cfun 1),
   21.59          (cont_tac 1),
   21.60          (rtac cont_Ispair2 1),
   21.61          (rtac cont2cont_CF1L 1),
   21.62          (rtac cont_Ispair1 1),
   21.63 -        (rtac (beta_cfun RS ssubst) 1),
   21.64 +        (stac beta_cfun 1),
   21.65          (rtac cont_Ispair2 1),
   21.66          (rtac refl 1)
   21.67          ]);
   21.68 @@ -366,7 +366,7 @@
   21.69  qed_goalw "strict_spair1" Sprod3.thy [spair_def] "(|UU,b|) = UU"
   21.70   (fn prems =>
   21.71          [
   21.72 -        (rtac (beta_cfun_sprod RS ssubst) 1),
   21.73 +        (stac beta_cfun_sprod 1),
   21.74          (rtac trans 1),
   21.75          (rtac (inst_sprod_pcpo RS sym) 2),
   21.76          (rtac strict_Ispair1 1)
   21.77 @@ -375,7 +375,7 @@
   21.78  qed_goalw "strict_spair2" Sprod3.thy [spair_def] "(|a,UU|) = UU"
   21.79   (fn prems =>
   21.80          [
   21.81 -        (rtac (beta_cfun_sprod RS ssubst) 1),
   21.82 +        (stac beta_cfun_sprod 1),
   21.83          (rtac trans 1),
   21.84          (rtac (inst_sprod_pcpo RS sym) 2),
   21.85          (rtac strict_Ispair2 1)
   21.86 @@ -408,8 +408,8 @@
   21.87   (fn prems =>
   21.88          [
   21.89          (cut_facts_tac prems 1),
   21.90 -        (rtac (beta_cfun_sprod RS ssubst) 1),
   21.91 -        (rtac (inst_sprod_pcpo RS ssubst) 1),
   21.92 +        (stac beta_cfun_sprod 1),
   21.93 +        (stac inst_sprod_pcpo 1),
   21.94          (etac defined_Ispair 1),
   21.95          (atac 1)
   21.96          ]);
   21.97 @@ -420,7 +420,7 @@
   21.98          [
   21.99          (rtac (Exh_Sprod RS disjE) 1),
  21.100          (rtac disjI1 1),
  21.101 -        (rtac (inst_sprod_pcpo RS ssubst) 1),
  21.102 +        (stac inst_sprod_pcpo 1),
  21.103          (atac 1),
  21.104          (rtac disjI2 1),
  21.105          (etac exE 1),
  21.106 @@ -428,7 +428,7 @@
  21.107          (rtac exI 1),
  21.108          (rtac exI 1),
  21.109          (rtac conjI 1),
  21.110 -        (rtac (beta_cfun_sprod RS ssubst) 1),
  21.111 +        (stac beta_cfun_sprod 1),
  21.112          (fast_tac HOL_cs 1),
  21.113          (fast_tac HOL_cs 1)
  21.114          ]);
  21.115 @@ -440,12 +440,12 @@
  21.116          [
  21.117          (rtac IsprodE 1),
  21.118          (resolve_tac prems 1),
  21.119 -        (rtac (inst_sprod_pcpo RS ssubst) 1),
  21.120 +        (stac inst_sprod_pcpo 1),
  21.121          (atac 1),
  21.122          (resolve_tac prems 1),
  21.123          (atac 2),
  21.124          (atac 2),
  21.125 -        (rtac (beta_cfun_sprod RS ssubst) 1),
  21.126 +        (stac beta_cfun_sprod 1),
  21.127          (atac 1)
  21.128          ]);
  21.129  
  21.130 @@ -455,7 +455,7 @@
  21.131   (fn prems =>
  21.132          [
  21.133          (cut_facts_tac prems 1),
  21.134 -        (rtac (beta_cfun RS ssubst) 1),
  21.135 +        (stac beta_cfun 1),
  21.136          (rtac cont_Isfst 1),
  21.137          (rtac strict_Isfst 1),
  21.138          (rtac (inst_sprod_pcpo RS subst) 1),
  21.139 @@ -466,8 +466,8 @@
  21.140          "sfst`(|UU,y|) = UU"
  21.141   (fn prems =>
  21.142          [
  21.143 -        (rtac (beta_cfun_sprod RS ssubst) 1),
  21.144 -        (rtac (beta_cfun RS ssubst) 1),
  21.145 +        (stac beta_cfun_sprod 1),
  21.146 +        (stac beta_cfun 1),
  21.147          (rtac cont_Isfst 1),
  21.148          (rtac strict_Isfst1 1)
  21.149          ]);
  21.150 @@ -476,8 +476,8 @@
  21.151          "sfst`(|x,UU|) = UU"
  21.152   (fn prems =>
  21.153          [
  21.154 -        (rtac (beta_cfun_sprod RS ssubst) 1),
  21.155 -        (rtac (beta_cfun RS ssubst) 1),
  21.156 +        (stac beta_cfun_sprod 1),
  21.157 +        (stac beta_cfun 1),
  21.158          (rtac cont_Isfst 1),
  21.159          (rtac strict_Isfst2 1)
  21.160          ]);
  21.161 @@ -487,7 +487,7 @@
  21.162   (fn prems =>
  21.163          [
  21.164          (cut_facts_tac prems 1),
  21.165 -        (rtac (beta_cfun RS ssubst) 1),
  21.166 +        (stac beta_cfun 1),
  21.167          (rtac cont_Issnd 1),
  21.168          (rtac strict_Issnd 1),
  21.169          (rtac (inst_sprod_pcpo RS subst) 1),
  21.170 @@ -498,8 +498,8 @@
  21.171          "ssnd`(|UU,y|) = UU"
  21.172   (fn prems =>
  21.173          [
  21.174 -        (rtac (beta_cfun_sprod RS ssubst) 1),
  21.175 -        (rtac (beta_cfun RS ssubst) 1),
  21.176 +        (stac beta_cfun_sprod 1),
  21.177 +        (stac beta_cfun 1),
  21.178          (rtac cont_Issnd 1),
  21.179          (rtac strict_Issnd1 1)
  21.180          ]);
  21.181 @@ -508,8 +508,8 @@
  21.182          "ssnd`(|x,UU|) = UU"
  21.183   (fn prems =>
  21.184          [
  21.185 -        (rtac (beta_cfun_sprod RS ssubst) 1),
  21.186 -        (rtac (beta_cfun RS ssubst) 1),
  21.187 +        (stac beta_cfun_sprod 1),
  21.188 +        (stac beta_cfun 1),
  21.189          (rtac cont_Issnd 1),
  21.190          (rtac strict_Issnd2 1)
  21.191          ]);
  21.192 @@ -519,8 +519,8 @@
  21.193   (fn prems =>
  21.194          [
  21.195          (cut_facts_tac prems 1),
  21.196 -        (rtac (beta_cfun_sprod RS ssubst) 1),
  21.197 -        (rtac (beta_cfun RS ssubst) 1),
  21.198 +        (stac beta_cfun_sprod 1),
  21.199 +        (stac beta_cfun 1),
  21.200          (rtac cont_Isfst 1),
  21.201          (etac Isfst2 1)
  21.202          ]);
  21.203 @@ -530,8 +530,8 @@
  21.204   (fn prems =>
  21.205          [
  21.206          (cut_facts_tac prems 1),
  21.207 -        (rtac (beta_cfun_sprod RS ssubst) 1),
  21.208 -        (rtac (beta_cfun RS ssubst) 1),
  21.209 +        (stac beta_cfun_sprod 1),
  21.210 +        (stac beta_cfun 1),
  21.211          (rtac cont_Issnd 1),
  21.212          (etac Issnd2 1)
  21.213          ]);
  21.214 @@ -542,9 +542,9 @@
  21.215   (fn prems =>
  21.216          [
  21.217          (cut_facts_tac prems 1),
  21.218 -        (rtac (beta_cfun RS ssubst) 1),
  21.219 +        (stac beta_cfun 1),
  21.220          (rtac cont_Issnd 1),
  21.221 -        (rtac (beta_cfun RS ssubst) 1),
  21.222 +        (stac beta_cfun 1),
  21.223          (rtac cont_Isfst 1),
  21.224          (rtac defined_IsfstIssnd 1),
  21.225          (rtac (inst_sprod_pcpo RS subst) 1),
  21.226 @@ -556,10 +556,10 @@
  21.227          [sfst_def,ssnd_def,spair_def] "(|sfst`p , ssnd`p|) = p"
  21.228   (fn prems =>
  21.229          [
  21.230 -        (rtac (beta_cfun_sprod RS ssubst) 1),
  21.231 -        (rtac (beta_cfun RS ssubst) 1),
  21.232 +        (stac beta_cfun_sprod 1),
  21.233 +        (stac beta_cfun 1),
  21.234          (rtac cont_Issnd 1),
  21.235 -        (rtac (beta_cfun RS ssubst) 1),
  21.236 +        (stac beta_cfun 1),
  21.237          (rtac cont_Isfst 1),
  21.238          (rtac (surjective_pairing_Sprod RS sym) 1)
  21.239          ]);
  21.240 @@ -570,13 +570,13 @@
  21.241   (fn prems =>
  21.242          [
  21.243          (cut_facts_tac prems 1),
  21.244 -        (rtac (beta_cfun RS ssubst) 1),
  21.245 +        (stac beta_cfun 1),
  21.246          (rtac cont_Issnd 1),
  21.247 -        (rtac (beta_cfun RS ssubst) 1),
  21.248 +        (stac beta_cfun 1),
  21.249          (rtac cont_Issnd 1),
  21.250 -        (rtac (beta_cfun RS ssubst) 1),
  21.251 +        (stac beta_cfun 1),
  21.252          (rtac cont_Isfst 1),
  21.253 -        (rtac (beta_cfun RS ssubst) 1),
  21.254 +        (stac beta_cfun 1),
  21.255          (rtac cont_Isfst 1),
  21.256          (rtac less_sprod3b 1),
  21.257          (rtac (inst_sprod_pcpo RS subst) 1),
  21.258 @@ -602,10 +602,10 @@
  21.259   (fn prems =>
  21.260          [
  21.261          (cut_facts_tac prems 1),
  21.262 -        (rtac (beta_cfun_sprod RS ssubst) 1),
  21.263 -        (rtac (beta_cfun RS ext RS ssubst) 1),
  21.264 +        (stac beta_cfun_sprod 1),
  21.265 +        (stac (beta_cfun RS ext) 1),
  21.266          (rtac cont_Issnd 1),
  21.267 -        (rtac (beta_cfun RS ext RS ssubst) 1),
  21.268 +        (stac (beta_cfun RS ext) 1),
  21.269          (rtac cont_Isfst 1),
  21.270          (rtac lub_sprod 1),
  21.271          (resolve_tac prems 1)
  21.272 @@ -623,9 +623,9 @@
  21.273          "ssplit`f`UU=UU"
  21.274   (fn prems =>
  21.275          [
  21.276 -        (rtac (beta_cfun RS ssubst) 1),
  21.277 +        (stac beta_cfun 1),
  21.278          (cont_tacR 1),
  21.279 -        (rtac (strictify1 RS ssubst) 1),
  21.280 +        (stac strictify1 1),
  21.281          (rtac refl 1)
  21.282          ]);
  21.283  
  21.284 @@ -633,17 +633,17 @@
  21.285          "[|x~=UU;y~=UU|] ==> ssplit`f`(|x,y|)= f`x`y"
  21.286   (fn prems =>
  21.287          [
  21.288 -        (rtac (beta_cfun RS ssubst) 1),
  21.289 +        (stac beta_cfun 1),
  21.290          (cont_tacR 1),
  21.291 -        (rtac (strictify2 RS ssubst) 1),
  21.292 +        (stac strictify2 1),
  21.293          (rtac defined_spair 1),
  21.294          (resolve_tac prems 1),
  21.295          (resolve_tac prems 1),
  21.296 -        (rtac (beta_cfun RS ssubst) 1),
  21.297 +        (stac beta_cfun 1),
  21.298          (cont_tacR 1),
  21.299 -        (rtac (sfst2 RS ssubst) 1),
  21.300 +        (stac sfst2 1),
  21.301          (resolve_tac prems 1),
  21.302 -        (rtac (ssnd2 RS ssubst) 1),
  21.303 +        (stac ssnd2 1),
  21.304          (resolve_tac prems 1),
  21.305          (rtac refl 1)
  21.306          ]);
  21.307 @@ -653,7 +653,7 @@
  21.308    "ssplit`spair`z=z"
  21.309   (fn prems =>
  21.310          [
  21.311 -        (rtac (beta_cfun RS ssubst) 1),
  21.312 +        (stac beta_cfun 1),
  21.313          (cont_tacR 1),
  21.314          (case_tac "z=UU" 1),
  21.315          (hyp_subst_tac 1),
  21.316 @@ -661,7 +661,7 @@
  21.317          (rtac trans 1),
  21.318          (rtac strictify2 1),
  21.319          (atac 1),
  21.320 -        (rtac (beta_cfun RS ssubst) 1),
  21.321 +        (stac beta_cfun 1),
  21.322          (cont_tacR 1),
  21.323          (rtac surjective_pairing_Sprod2 1)
  21.324          ]);
    22.1 --- a/src/HOLCF/Ssum2.ML	Thu Sep 26 12:50:48 1996 +0200
    22.2 +++ b/src/HOLCF/Ssum2.ML	Thu Sep 26 15:14:23 1996 +0200
    22.3 @@ -16,7 +16,7 @@
    22.4          "(Isinl(x) << Isinl(y)) = (x << y)"
    22.5   (fn prems =>
    22.6          [
    22.7 -        (rtac (inst_ssum_po RS ssubst) 1),
    22.8 +        (stac inst_ssum_po 1),
    22.9          (rtac less_ssum2a 1)
   22.10          ]);
   22.11  
   22.12 @@ -24,7 +24,7 @@
   22.13          "(Isinr(x) << Isinr(y)) = (x << y)"
   22.14   (fn prems =>
   22.15          [
   22.16 -        (rtac (inst_ssum_po RS ssubst) 1),
   22.17 +        (stac inst_ssum_po 1),
   22.18          (rtac less_ssum2b 1)
   22.19          ]);
   22.20  
   22.21 @@ -32,7 +32,7 @@
   22.22          "(Isinl(x) << Isinr(y)) = (x = UU)"
   22.23   (fn prems =>
   22.24          [
   22.25 -        (rtac (inst_ssum_po RS ssubst) 1),
   22.26 +        (stac inst_ssum_po 1),
   22.27          (rtac less_ssum2c 1)
   22.28          ]);
   22.29  
   22.30 @@ -40,7 +40,7 @@
   22.31          "(Isinr(x) << Isinl(y)) = (x = UU)"
   22.32   (fn prems =>
   22.33          [
   22.34 -        (rtac (inst_ssum_po RS ssubst) 1),
   22.35 +        (stac inst_ssum_po 1),
   22.36          (rtac less_ssum2d 1)
   22.37          ]);
   22.38  
   22.39 @@ -57,7 +57,7 @@
   22.40          (rtac (less_ssum3a RS iffD2) 1),
   22.41          (rtac minimal 1),
   22.42          (hyp_subst_tac 1),
   22.43 -        (rtac (strict_IsinlIsinr RS ssubst) 1),
   22.44 +        (stac strict_IsinlIsinr 1),
   22.45          (rtac (less_ssum3b RS iffD2) 1),
   22.46          (rtac minimal 1)
   22.47          ]);
    23.1 --- a/src/HOLCF/Ssum3.ML	Thu Sep 26 12:50:48 1996 +0200
    23.2 +++ b/src/HOLCF/Ssum3.ML	Thu Sep 26 15:14:23 1996 +0200
    23.3 @@ -226,7 +226,7 @@
    23.4          (rtac (chain_mono2 RS exE) 1),
    23.5          (atac 2),
    23.6          (rtac chain_UU_I_inverse2 1),
    23.7 -        (rtac (inst_ssum_pcpo RS ssubst) 1),
    23.8 +        (stac inst_ssum_pcpo 1),
    23.9          (etac swap 1),
   23.10          (rtac inject_Isinl 1),
   23.11          (rtac trans 1),
   23.12 @@ -244,14 +244,14 @@
   23.13          (rtac Iwhen2 1),
   23.14          (res_inst_tac [("Pa","Y(i)=UU")] swap 1),
   23.15          (fast_tac HOL_cs 1),
   23.16 -        (rtac (inst_ssum_pcpo RS ssubst) 1),
   23.17 +        (stac inst_ssum_pcpo 1),
   23.18          (res_inst_tac [("t","Y(i)")] ssubst 1),
   23.19          (atac 1),
   23.20          (fast_tac HOL_cs 1),
   23.21 -        (rtac (Iwhen2 RS ssubst) 1),
   23.22 +        (stac Iwhen2 1),
   23.23          (res_inst_tac [("Pa","Y(i)=UU")] swap 1),
   23.24          (fast_tac HOL_cs 1),
   23.25 -        (rtac (inst_ssum_pcpo RS ssubst) 1),
   23.26 +        (stac inst_ssum_pcpo 1),
   23.27          (res_inst_tac [("t","Y(i)")] ssubst 1),
   23.28          (atac 1),
   23.29          (fast_tac HOL_cs 1),
   23.30 @@ -285,7 +285,7 @@
   23.31          (rtac (chain_mono2 RS exE) 1),
   23.32          (atac 2),
   23.33          (rtac chain_UU_I_inverse2 1),
   23.34 -        (rtac (inst_ssum_pcpo RS ssubst) 1),
   23.35 +        (stac inst_ssum_pcpo 1),
   23.36          (etac swap 1),
   23.37          (rtac inject_Isinr 1),
   23.38          (rtac trans 1),
   23.39 @@ -305,17 +305,17 @@
   23.40          (res_inst_tac [("Pa","Y(i)=UU")] swap 1),
   23.41          (fast_tac HOL_cs 1),
   23.42          (dtac notnotD 1),
   23.43 -        (rtac (inst_ssum_pcpo RS ssubst) 1),
   23.44 -        (rtac (strict_IsinlIsinr RS ssubst) 1),
   23.45 +        (stac inst_ssum_pcpo 1),
   23.46 +        (stac strict_IsinlIsinr 1),
   23.47          (res_inst_tac [("t","Y(i)")] ssubst 1),
   23.48          (atac 1),
   23.49          (fast_tac HOL_cs 1),
   23.50 -        (rtac (Iwhen3 RS ssubst) 1),
   23.51 +        (stac Iwhen3 1),
   23.52          (res_inst_tac [("Pa","Y(i)=UU")] swap 1),
   23.53          (fast_tac HOL_cs 1),
   23.54          (dtac notnotD 1),
   23.55 -        (rtac (inst_ssum_pcpo RS ssubst) 1),
   23.56 -        (rtac (strict_IsinlIsinr RS ssubst) 1),
   23.57 +        (stac inst_ssum_pcpo 1),
   23.58 +        (stac strict_IsinlIsinr 1),
   23.59          (res_inst_tac [("t","Y(i)")] ssubst 1),
   23.60          (atac 1),
   23.61          (fast_tac HOL_cs 1),
   23.62 @@ -425,7 +425,7 @@
   23.63          (cut_facts_tac prems 1),
   23.64          (etac swap 1),
   23.65          (rtac inject_sinl 1),
   23.66 -        (rtac (strict_sinl RS ssubst) 1),
   23.67 +        (stac strict_sinl 1),
   23.68          (etac notnotD 1)
   23.69          ]);
   23.70  
   23.71 @@ -436,7 +436,7 @@
   23.72          (cut_facts_tac prems 1),
   23.73          (etac swap 1),
   23.74          (rtac inject_sinr 1),
   23.75 -        (rtac (strict_sinr RS ssubst) 1),
   23.76 +        (stac strict_sinr 1),
   23.77          (etac notnotD 1)
   23.78          ]);
   23.79  
   23.80 @@ -445,7 +445,7 @@
   23.81   (fn prems =>
   23.82          [
   23.83          (asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1),
   23.84 -        (rtac (inst_ssum_pcpo RS ssubst) 1),
   23.85 +        (stac inst_ssum_pcpo 1),
   23.86          (rtac Exh_Ssum 1)
   23.87          ]);
   23.88  
   23.89 @@ -458,7 +458,7 @@
   23.90          [
   23.91          (rtac IssumE 1),
   23.92          (resolve_tac prems 1),
   23.93 -        (rtac (inst_ssum_pcpo RS ssubst) 1),
   23.94 +        (stac inst_ssum_pcpo 1),
   23.95          (atac 1),
   23.96          (resolve_tac prems 1),
   23.97          (atac 2),
   23.98 @@ -476,11 +476,11 @@
   23.99          [
  23.100          (rtac IssumE2 1),
  23.101          (resolve_tac prems 1),
  23.102 -        (rtac (beta_cfun RS ssubst) 1),
  23.103 +        (stac beta_cfun 1),
  23.104          (rtac cont_Isinl 1),
  23.105          (atac 1),
  23.106          (resolve_tac prems 1),
  23.107 -        (rtac (beta_cfun RS ssubst) 1),
  23.108 +        (stac beta_cfun 1),
  23.109          (rtac cont_Isinr 1),
  23.110          (atac 1)
  23.111          ]);
  23.112 @@ -489,14 +489,14 @@
  23.113          "sswhen`f`g`UU = UU"
  23.114   (fn prems =>
  23.115          [
  23.116 -        (rtac (inst_ssum_pcpo RS ssubst) 1),
  23.117 -        (rtac (beta_cfun RS ssubst) 1),
  23.118 +        (stac inst_ssum_pcpo 1),
  23.119 +        (stac beta_cfun 1),
  23.120          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.121                  cont_Iwhen3,cont2cont_CF1L]) 1)),
  23.122 -        (rtac (beta_cfun RS ssubst) 1),
  23.123 +        (stac beta_cfun 1),
  23.124          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.125                  cont_Iwhen3,cont2cont_CF1L]) 1)),
  23.126 -        (rtac (beta_cfun RS ssubst) 1),
  23.127 +        (stac beta_cfun 1),
  23.128          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.129                  cont_Iwhen3,cont2cont_CF1L]) 1)),
  23.130          (simp_tac Ssum0_ss  1)
  23.131 @@ -507,16 +507,16 @@
  23.132   (fn prems =>
  23.133          [
  23.134          (cut_facts_tac prems 1),
  23.135 -        (rtac (beta_cfun RS ssubst) 1),
  23.136 +        (stac beta_cfun 1),
  23.137          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.138                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.139 -        (rtac (beta_cfun RS ssubst) 1),
  23.140 +        (stac beta_cfun 1),
  23.141          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.142                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.143 -        (rtac (beta_cfun RS ssubst) 1),
  23.144 +        (stac beta_cfun 1),
  23.145          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.146                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.147 -        (rtac (beta_cfun RS ssubst) 1),
  23.148 +        (stac beta_cfun 1),
  23.149          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.150                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.151          (asm_simp_tac Ssum0_ss  1)
  23.152 @@ -529,16 +529,16 @@
  23.153   (fn prems =>
  23.154          [
  23.155          (cut_facts_tac prems 1),
  23.156 -        (rtac (beta_cfun RS ssubst) 1),
  23.157 +        (stac beta_cfun 1),
  23.158          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.159                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.160 -        (rtac (beta_cfun RS ssubst) 1),
  23.161 +        (stac beta_cfun 1),
  23.162          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.163                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.164 -        (rtac (beta_cfun RS ssubst) 1),
  23.165 +        (stac beta_cfun 1),
  23.166          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.167                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.168 -        (rtac (beta_cfun RS ssubst) 1),
  23.169 +        (stac beta_cfun 1),
  23.170          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.171                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.172          (asm_simp_tac Ssum0_ss  1)
  23.173 @@ -549,10 +549,10 @@
  23.174          "(sinl`x << sinl`y) = (x << y)"
  23.175   (fn prems =>
  23.176          [
  23.177 -        (rtac (beta_cfun RS ssubst) 1),
  23.178 +        (stac beta_cfun 1),
  23.179          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.180                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.181 -        (rtac (beta_cfun RS ssubst) 1),
  23.182 +        (stac beta_cfun 1),
  23.183          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.184                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.185          (rtac less_ssum3a 1)
  23.186 @@ -562,10 +562,10 @@
  23.187          "(sinr`x << sinr`y) = (x << y)"
  23.188   (fn prems =>
  23.189          [
  23.190 -        (rtac (beta_cfun RS ssubst) 1),
  23.191 +        (stac beta_cfun 1),
  23.192          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.193                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.194 -        (rtac (beta_cfun RS ssubst) 1),
  23.195 +        (stac beta_cfun 1),
  23.196          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.197                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.198          (rtac less_ssum3b 1)
  23.199 @@ -575,10 +575,10 @@
  23.200          "(sinl`x << sinr`y) = (x = UU)"
  23.201   (fn prems =>
  23.202          [
  23.203 -        (rtac (beta_cfun RS ssubst) 1),
  23.204 +        (stac beta_cfun 1),
  23.205          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.206                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.207 -        (rtac (beta_cfun RS ssubst) 1),
  23.208 +        (stac beta_cfun 1),
  23.209          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.210                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.211          (rtac less_ssum3c 1)
  23.212 @@ -588,10 +588,10 @@
  23.213          "(sinr`x << sinl`y) = (x = UU)"
  23.214   (fn prems =>
  23.215          [
  23.216 -        (rtac (beta_cfun RS ssubst) 1),
  23.217 +        (stac beta_cfun 1),
  23.218          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.219                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.220 -        (rtac (beta_cfun RS ssubst) 1),
  23.221 +        (stac beta_cfun 1),
  23.222          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.223                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.224          (rtac less_ssum3d 1)
  23.225 @@ -613,13 +613,13 @@
  23.226   (fn prems =>
  23.227          [
  23.228          (cut_facts_tac prems 1),
  23.229 -        (rtac (beta_cfun RS ssubst) 1),
  23.230 +        (stac beta_cfun 1),
  23.231          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,           cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.232 -        (rtac (beta_cfun RS ssubst) 1),
  23.233 +        (stac beta_cfun 1),
  23.234          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,           cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.235 -        (rtac (beta_cfun RS ssubst) 1),
  23.236 +        (stac beta_cfun 1),
  23.237          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,           cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.238 -        (rtac (beta_cfun RS ext RS ssubst) 1),
  23.239 +        (stac (beta_cfun RS ext) 1),
  23.240          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,           cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.241          (rtac thelub_ssum1a 1),
  23.242          (atac 1),
  23.243 @@ -638,16 +638,16 @@
  23.244   (fn prems =>
  23.245          [
  23.246          (cut_facts_tac prems 1),
  23.247 -        (rtac (beta_cfun RS ssubst) 1),
  23.248 +        (stac beta_cfun 1),
  23.249          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.250                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.251 -        (rtac (beta_cfun RS ssubst) 1),
  23.252 +        (stac beta_cfun 1),
  23.253          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.254                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.255 -        (rtac (beta_cfun RS ssubst) 1),
  23.256 +        (stac beta_cfun 1),
  23.257          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.258                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.259 -        (rtac (beta_cfun RS ext RS ssubst) 1),
  23.260 +        (stac (beta_cfun RS ext) 1),
  23.261          (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
  23.262                  cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
  23.263          (rtac thelub_ssum1b 1),
    24.1 --- a/src/HOLCF/Tr1.ML	Thu Sep 26 12:50:48 1996 +0200
    24.2 +++ b/src/HOLCF/Tr1.ML	Thu Sep 26 15:14:23 1996 +0200
    24.3 @@ -23,7 +23,7 @@
    24.4          (rtac (rep_tr_iso RS subst) 1),
    24.5          (rtac (rep_tr_iso RS subst) 1),
    24.6          (rtac cfun_arg_cong 1),
    24.7 -        (rtac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict )            RS conjunct2 RS ssubst) 1),
    24.8 +        (stac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict )            RS conjunct2) 1),
    24.9          (etac (eq_UU_iff RS ssubst) 1)
   24.10          ]),
   24.11  prove_goalw Tr1.thy [FF_def] "~FF << UU"
   24.12 @@ -36,7 +36,7 @@
   24.13          (rtac (rep_tr_iso RS subst) 1),
   24.14          (rtac (rep_tr_iso RS subst) 1),
   24.15          (rtac cfun_arg_cong 1),
   24.16 -        (rtac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict )            RS conjunct2 RS ssubst) 1),
   24.17 +        (stac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict )            RS conjunct2) 1),
   24.18          (etac (eq_UU_iff RS ssubst) 1)
   24.19          ]),
   24.20  prove_goalw Tr1.thy [FF_def,TT_def] "~TT << FF"
    25.1 --- a/src/HOLCF/Void.ML	Thu Sep 26 12:50:48 1996 +0200
    25.2 +++ b/src/HOLCF/Void.ML	Thu Sep 26 15:14:23 1996 +0200
    25.3 @@ -19,7 +19,7 @@
    25.4   " UU_void_Rep : Void"
    25.5  (fn prems =>
    25.6          [
    25.7 -        (rtac (mem_Collect_eq RS ssubst) 1),
    25.8 +        (stac mem_Collect_eq 1),
    25.9          (rtac refl 1)
   25.10          ]);
   25.11  
    26.1 --- a/src/HOLCF/ccc1.ML	Thu Sep 26 12:50:48 1996 +0200
    26.2 +++ b/src/HOLCF/ccc1.ML	Thu Sep 26 15:14:23 1996 +0200
    26.3 @@ -17,7 +17,7 @@
    26.4  qed_goalw "ID1" ccc1.thy [ID_def] "ID`x=x"
    26.5   (fn prems =>
    26.6          [
    26.7 -        (rtac (beta_cfun RS ssubst) 1),
    26.8 +        (stac beta_cfun 1),
    26.9          (rtac cont_id 1),
   26.10          (rtac refl 1)
   26.11          ]);
   26.12 @@ -25,9 +25,9 @@
   26.13  qed_goalw "cfcomp1" ccc1.thy [oo_def] "(f oo g)=(LAM x.f`(g`x))"
   26.14   (fn prems =>
   26.15          [
   26.16 -        (rtac (beta_cfun RS ssubst) 1),
   26.17 +        (stac beta_cfun 1),
   26.18          (cont_tacR 1),
   26.19 -        (rtac (beta_cfun RS ssubst) 1),
   26.20 +        (stac beta_cfun 1),
   26.21          (cont_tacR 1),
   26.22          (rtac refl 1)
   26.23          ]);
   26.24 @@ -35,8 +35,8 @@
   26.25  qed_goal "cfcomp2" ccc1.thy  "(f oo g)`x=f`(g`x)"
   26.26   (fn prems =>
   26.27          [
   26.28 -        (rtac (cfcomp1 RS ssubst) 1),
   26.29 -        (rtac (beta_cfun RS ssubst) 1),
   26.30 +        (stac cfcomp1 1),
   26.31 +        (stac beta_cfun 1),
   26.32          (cont_tacR 1),
   26.33          (rtac refl 1)
   26.34          ]);
   26.35 @@ -55,8 +55,8 @@
   26.36   (fn prems =>
   26.37          [
   26.38          (rtac ext_cfun 1),
   26.39 -        (rtac  (cfcomp2 RS ssubst) 1),
   26.40 -        (rtac  (ID1 RS ssubst) 1),
   26.41 +        (stac cfcomp2 1),
   26.42 +        (stac ID1 1),
   26.43          (rtac refl 1)
   26.44          ]);
   26.45  
   26.46 @@ -64,8 +64,8 @@
   26.47   (fn prems =>
   26.48          [
   26.49          (rtac ext_cfun 1),
   26.50 -        (rtac  (cfcomp2 RS ssubst) 1),
   26.51 -        (rtac  (ID1 RS ssubst) 1),
   26.52 +        (stac cfcomp2 1),
   26.53 +        (stac ID1 1),
   26.54          (rtac refl 1)
   26.55          ]);
   26.56  
   26.57 @@ -75,11 +75,11 @@
   26.58          [
   26.59          (rtac ext_cfun 1),
   26.60          (res_inst_tac [("s","f`(g`(h`x))")] trans  1),
   26.61 -        (rtac  (cfcomp2 RS ssubst) 1),
   26.62 -        (rtac  (cfcomp2 RS ssubst) 1),
   26.63 +        (stac cfcomp2 1),
   26.64 +        (stac cfcomp2 1),
   26.65          (rtac refl 1),
   26.66 -        (rtac  (cfcomp2 RS ssubst) 1),
   26.67 -        (rtac  (cfcomp2 RS ssubst) 1),
   26.68 +        (stac cfcomp2 1),
   26.69 +        (stac cfcomp2 1),
   26.70          (rtac refl 1)
   26.71          ]);
   26.72  
    27.1 --- a/src/HOLCF/domain/theorems.ML	Thu Sep 26 12:50:48 1996 +0200
    27.2 +++ b/src/HOLCF/domain/theorems.ML	Thu Sep 26 15:14:23 1996 +0200
    27.3 @@ -29,56 +29,56 @@
    27.4  (* ----- general proof facilities ------------------------------------------- *)
    27.5  
    27.6  fun inferT sg pre_tm = #2 (Sign.infer_types sg (K None) (K None) [] true 
    27.7 -			   ([pre_tm],propT));
    27.8 +                           ([pre_tm],propT));
    27.9  
   27.10  fun pg'' thy defs t = let val sg = sign_of thy;
   27.11 -		          val ct = Thm.cterm_of sg (inferT sg t);
   27.12 -		      in prove_goalw_cterm defs ct end;
   27.13 +                          val ct = Thm.cterm_of sg (inferT sg t);
   27.14 +                      in prove_goalw_cterm defs ct end;
   27.15  fun pg'  thy defs t tacsf=pg'' thy defs t (fn []   => tacsf 
   27.16 -				| prems=> (cut_facts_tac prems 1)::tacsf);
   27.17 +                                | prems=> (cut_facts_tac prems 1)::tacsf);
   27.18  
   27.19  fun REPEAT_DETERM_UNTIL p tac = 
   27.20  let fun drep st = if p st then Sequence.single st
   27.21 -			  else (case Sequence.pull(tac st) of
   27.22 -		                  None        => Sequence.null
   27.23 -				| Some(st',_) => drep st')
   27.24 +                          else (case Sequence.pull(tac st) of
   27.25 +                                  None        => Sequence.null
   27.26 +                                | Some(st',_) => drep st')
   27.27  in drep end;
   27.28  val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);
   27.29  
   27.30  local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn _ => [rtac TrueI 1]) in
   27.31  val kill_neq_tac = dtac trueI2 end;
   27.32 -fun case_UU_tac rews i v =	case_tac (v^"=UU") i THEN
   27.33 -				asm_simp_tac (HOLCF_ss addsimps rews) i;
   27.34 +fun case_UU_tac rews i v =      case_tac (v^"=UU") i THEN
   27.35 +                                asm_simp_tac (HOLCF_ss addsimps rews) i;
   27.36  
   27.37  val chain_tac = REPEAT_DETERM o resolve_tac 
   27.38 -		[is_chain_iterate, ch2ch_fappR, ch2ch_fappL];
   27.39 +                [is_chain_iterate, ch2ch_fappR, ch2ch_fappL];
   27.40  
   27.41  (* ----- general proofs ----------------------------------------------------- *)
   27.42  
   27.43  val quant_ss = HOL_ss addsimps (map (fn s => prove_goal HOL.thy s (fn _ =>[
   27.44 -		fast_tac HOL_cs 1]))["(!x. P x & Q)=((!x. P x) & Q)",
   27.45 -			    	     "(!x. P & Q x) = (P & (!x. Q x))"]);
   27.46 +                fast_tac HOL_cs 1]))["(!x. P x & Q)=((!x. P x) & Q)",
   27.47 +                                     "(!x. P & Q x) = (P & (!x. Q x))"]);
   27.48  
   27.49  val all2E = prove_goal HOL.thy "[| !x y . P x y; P x y ==> R |] ==> R"
   27.50   (fn prems =>[
   27.51 -				resolve_tac prems 1,
   27.52 -				cut_facts_tac prems 1,
   27.53 -				fast_tac HOL_cs 1]);
   27.54 +                                resolve_tac prems 1,
   27.55 +                                cut_facts_tac prems 1,
   27.56 +                                fast_tac HOL_cs 1]);
   27.57  
   27.58  val swap3 = prove_goal HOL.thy "[| Q ==> P; ~P |] ==> ~Q" (fn prems => [
   27.59                                  cut_facts_tac prems 1,
   27.60                                  etac swap 1,
   27.61                                  dtac notnotD 1,
   27.62 -				etac (hd prems) 1]);
   27.63 +                                etac (hd prems) 1]);
   27.64  
   27.65  val dist_eqI = prove_goal Porder.thy "~ x << y ==> x ~= y" (fn prems => [
   27.66                                  rtac swap3 1,
   27.67 -				etac (antisym_less_inverse RS conjunct1) 1,
   27.68 -				resolve_tac prems 1]);
   27.69 +                                etac (antisym_less_inverse RS conjunct1) 1,
   27.70 +                                resolve_tac prems 1]);
   27.71  val cfst_strict  = prove_goal Cprod3.thy "cfst`UU = UU" (fn _ => [
   27.72 -			(simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
   27.73 +                        (simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
   27.74  val csnd_strict  = prove_goal Cprod3.thy "csnd`UU = UU" (fn _ => [
   27.75 -			(simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
   27.76 +                        (simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
   27.77  
   27.78  in
   27.79  
   27.80 @@ -93,8 +93,8 @@
   27.81  val b = 0;
   27.82  fun _ y t = by t;
   27.83  fun  g  defs t = let val sg = sign_of thy;
   27.84 -		     val ct = Thm.cterm_of sg (inferT sg t);
   27.85 -		 in goalw_cterm defs ct end;
   27.86 +                     val ct = Thm.cterm_of sg (inferT sg t);
   27.87 +                 in goalw_cterm defs ct end;
   27.88  *)
   27.89  
   27.90  
   27.91 @@ -107,7 +107,7 @@
   27.92  val axs_con_def   = map (fn (con,_) => ga (extern_name con ^"_def")) cons;
   27.93  val axs_dis_def   = map (fn (con,_) => ga (   dis_name con ^"_def")) cons;
   27.94  val axs_sel_def   = flat(map (fn (_,args) => 
   27.95 -		    map (fn     arg => ga (sel_of arg      ^"_def")) args)cons);
   27.96 +                    map (fn     arg => ga (sel_of arg      ^"_def")) args)cons);
   27.97  val ax_copy_def   = ga (dname^"_copy_def"  );
   27.98  end; (* local *)
   27.99  
  27.100 @@ -119,71 +119,71 @@
  27.101  val x_name = "x";
  27.102  
  27.103  val (rep_strict, abs_strict) = let 
  27.104 -	 val r = ax_rep_iso RS (ax_abs_iso RS (allI  RSN(2,allI RS iso_strict)))
  27.105 -	       in (r RS conjunct1, r RS conjunct2) end;
  27.106 +         val r = ax_rep_iso RS (ax_abs_iso RS (allI  RSN(2,allI RS iso_strict)))
  27.107 +               in (r RS conjunct1, r RS conjunct2) end;
  27.108  val abs_defin' = pg [] ((dc_abs`%x_name === UU) ==> (%x_name === UU)) [
  27.109 -			   res_inst_tac [("t",x_name)] (ax_abs_iso RS subst) 1,
  27.110 -				etac ssubst 1, rtac rep_strict 1];
  27.111 +                           res_inst_tac [("t",x_name)] (ax_abs_iso RS subst) 1,
  27.112 +                                etac ssubst 1, rtac rep_strict 1];
  27.113  val rep_defin' = pg [] ((dc_rep`%x_name === UU) ==> (%x_name === UU)) [
  27.114 -			   res_inst_tac [("t",x_name)] (ax_rep_iso RS subst) 1,
  27.115 -				etac ssubst 1, rtac abs_strict 1];
  27.116 +                           res_inst_tac [("t",x_name)] (ax_rep_iso RS subst) 1,
  27.117 +                                etac ssubst 1, rtac abs_strict 1];
  27.118  val iso_rews = [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
  27.119  
  27.120  local 
  27.121  val iso_swap = pg [] (dc_rep`%"x" === %"y" ==> %"x" === dc_abs`%"y") [
  27.122 -			    dres_inst_tac [("f",dname^"_abs")] cfun_arg_cong 1,
  27.123 -			    etac (ax_rep_iso RS subst) 1];
  27.124 +                            dres_inst_tac [("f",dname^"_abs")] cfun_arg_cong 1,
  27.125 +                            etac (ax_rep_iso RS subst) 1];
  27.126  fun exh foldr1 cn quant foldr2 var = let
  27.127    fun one_con (con,args) = let val vns = map vname args in
  27.128      foldr quant (vns, foldr2 ((%x_name === con_app2 con (var vns) vns)::
  27.129 -			      map (defined o (var vns)) (nonlazy args))) end
  27.130 +                              map (defined o (var vns)) (nonlazy args))) end
  27.131    in foldr1 ((cn(%x_name===UU))::map one_con cons) end;
  27.132  in
  27.133  val cases = let 
  27.134 -	    fun common_tac thm = rtac thm 1 THEN contr_tac 1;
  27.135 -	    fun unit_tac true = common_tac liftE1
  27.136 -	    |   unit_tac _    = all_tac;
  27.137 -	    fun prod_tac []          = common_tac oneE
  27.138 -	    |   prod_tac [arg]       = unit_tac (is_lazy arg)
  27.139 -	    |   prod_tac (arg::args) = 
  27.140 -				common_tac sprodE THEN
  27.141 -				kill_neq_tac 1 THEN
  27.142 -				unit_tac (is_lazy arg) THEN
  27.143 -				prod_tac args;
  27.144 -	    fun sum_rest_tac p = SELECT_GOAL(EVERY[
  27.145 -				rtac p 1,
  27.146 -				rewrite_goals_tac axs_con_def,
  27.147 -				dtac iso_swap 1,
  27.148 -				simp_tac HOLCF_ss 1,
  27.149 -				UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1;
  27.150 -	    fun sum_tac [(_,args)]       [p]        = 
  27.151 -				prod_tac args THEN sum_rest_tac p
  27.152 -	    |   sum_tac ((_,args)::cons') (p::prems) = DETERM(
  27.153 -				common_tac ssumE THEN
  27.154 -				kill_neq_tac 1 THEN kill_neq_tac 2 THEN
  27.155 -				prod_tac args THEN sum_rest_tac p) THEN
  27.156 -				sum_tac cons' prems
  27.157 -	    |   sum_tac _ _ = Imposs "theorems:sum_tac";
  27.158 -	  in pg'' thy [] (exh (fn l => foldr (op ===>) (l,mk_trp(%"P")))
  27.159 -			      (fn T => T ==> %"P") mk_All
  27.160 -			      (fn l => foldr (op ===>) (map mk_trp l,
  27.161 -							    mk_trp(%"P")))
  27.162 -			      bound_arg)
  27.163 -			     (fn prems => [
  27.164 -				cut_facts_tac [excluded_middle] 1,
  27.165 -				etac disjE 1,
  27.166 -				rtac (hd prems) 2,
  27.167 -				etac rep_defin' 2,
  27.168 -				if length cons = 1 andalso 
  27.169 -				   length (snd(hd cons)) = 1 andalso 
  27.170 -				   not(is_lazy(hd(snd(hd cons))))
  27.171 -				then rtac (hd (tl prems)) 1 THEN atac 2 THEN
  27.172 -				     rewrite_goals_tac axs_con_def THEN
  27.173 -				     simp_tac (HOLCF_ss addsimps [ax_rep_iso]) 1
  27.174 -				else sum_tac cons (tl prems)])end;
  27.175 +            fun common_tac thm = rtac thm 1 THEN contr_tac 1;
  27.176 +            fun unit_tac true = common_tac liftE1
  27.177 +            |   unit_tac _    = all_tac;
  27.178 +            fun prod_tac []          = common_tac oneE
  27.179 +            |   prod_tac [arg]       = unit_tac (is_lazy arg)
  27.180 +            |   prod_tac (arg::args) = 
  27.181 +                                common_tac sprodE THEN
  27.182 +                                kill_neq_tac 1 THEN
  27.183 +                                unit_tac (is_lazy arg) THEN
  27.184 +                                prod_tac args;
  27.185 +            fun sum_rest_tac p = SELECT_GOAL(EVERY[
  27.186 +                                rtac p 1,
  27.187 +                                rewrite_goals_tac axs_con_def,
  27.188 +                                dtac iso_swap 1,
  27.189 +                                simp_tac HOLCF_ss 1,
  27.190 +                                UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1;
  27.191 +            fun sum_tac [(_,args)]       [p]        = 
  27.192 +                                prod_tac args THEN sum_rest_tac p
  27.193 +            |   sum_tac ((_,args)::cons') (p::prems) = DETERM(
  27.194 +                                common_tac ssumE THEN
  27.195 +                                kill_neq_tac 1 THEN kill_neq_tac 2 THEN
  27.196 +                                prod_tac args THEN sum_rest_tac p) THEN
  27.197 +                                sum_tac cons' prems
  27.198 +            |   sum_tac _ _ = Imposs "theorems:sum_tac";
  27.199 +          in pg'' thy [] (exh (fn l => foldr (op ===>) (l,mk_trp(%"P")))
  27.200 +                              (fn T => T ==> %"P") mk_All
  27.201 +                              (fn l => foldr (op ===>) (map mk_trp l,
  27.202 +                                                            mk_trp(%"P")))
  27.203 +                              bound_arg)
  27.204 +                             (fn prems => [
  27.205 +                                cut_facts_tac [excluded_middle] 1,
  27.206 +                                etac disjE 1,
  27.207 +                                rtac (hd prems) 2,
  27.208 +                                etac rep_defin' 2,
  27.209 +                                if length cons = 1 andalso 
  27.210 +                                   length (snd(hd cons)) = 1 andalso 
  27.211 +                                   not(is_lazy(hd(snd(hd cons))))
  27.212 +                                then rtac (hd (tl prems)) 1 THEN atac 2 THEN
  27.213 +                                     rewrite_goals_tac axs_con_def THEN
  27.214 +                                     simp_tac (HOLCF_ss addsimps [ax_rep_iso]) 1
  27.215 +                                else sum_tac cons (tl prems)])end;
  27.216  val exhaust= pg[](mk_trp(exh (foldr' mk_disj) Id mk_ex (foldr' mk_conj) (K %)))[
  27.217 -				rtac cases 1,
  27.218 -				UNTIL_SOLVED(fast_tac HOL_cs 1)];
  27.219 +                                rtac cases 1,
  27.220 +                                UNTIL_SOLVED(fast_tac HOL_cs 1)];
  27.221  end;
  27.222  
  27.223  local 
  27.224 @@ -191,17 +191,17 @@
  27.225    fun bound_fun i _ = Bound (length cons - i);
  27.226    val when_app  = foldl (op `) (%%(dname^"_when"), mapn bound_fun 1 cons);
  27.227    val when_appl = pg [ax_when_def] (bind_fun(mk_trp(when_app`%x_name ===
  27.228 -	     when_body cons (fn (m,n)=> bound_fun (n-m) 0)`(dc_rep`%x_name))))[
  27.229 -				simp_tac HOLCF_ss 1];
  27.230 +             when_body cons (fn (m,n)=> bound_fun (n-m) 0)`(dc_rep`%x_name))))[
  27.231 +                                simp_tac HOLCF_ss 1];
  27.232  in
  27.233  val when_strict = pg [] (bind_fun(mk_trp(strict when_app))) [
  27.234 -			simp_tac(HOLCF_ss addsimps [when_appl,rep_strict]) 1];
  27.235 +                        simp_tac(HOLCF_ss addsimps [when_appl,rep_strict]) 1];
  27.236  val when_apps = let fun one_when n (con,args) = pg axs_con_def 
  27.237 -		(bind_fun (lift_defined % (nonlazy args, 
  27.238 -		mk_trp(when_app`(con_app con args) ===
  27.239 +                (bind_fun (lift_defined % (nonlazy args, 
  27.240 +                mk_trp(when_app`(con_app con args) ===
  27.241                         mk_cfapp(bound_fun n 0,map %# args)))))[
  27.242 -		asm_simp_tac (HOLCF_ss addsimps [when_appl,ax_abs_iso]) 1];
  27.243 -	in mapn one_when 1 cons end;
  27.244 +                asm_simp_tac (HOLCF_ss addsimps [when_appl,ax_abs_iso]) 1];
  27.245 +        in mapn one_when 1 cons end;
  27.246  end;
  27.247  val when_rews = when_strict::when_apps;
  27.248  
  27.249 @@ -209,143 +209,143 @@
  27.250  
  27.251  val dis_rews = let
  27.252    val dis_stricts = map (fn (con,_) => pg axs_dis_def (mk_trp(
  27.253 -		      	     strict(%%(dis_name con)))) [
  27.254 -				simp_tac (HOLCF_ss addsimps when_rews) 1]) cons;
  27.255 +                             strict(%%(dis_name con)))) [
  27.256 +                                simp_tac (HOLCF_ss addsimps when_rews) 1]) cons;
  27.257    val dis_apps = let fun one_dis c (con,args)= pg axs_dis_def
  27.258 -		   (lift_defined % (nonlazy args,
  27.259 -			(mk_trp((%%(dis_name c))`(con_app con args) ===
  27.260 -			      %%(if con=c then "TT" else "FF"))))) [
  27.261 -				asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
  27.262 -	in flat(map (fn (c,_) => map (one_dis c) cons) cons) end;
  27.263 +                   (lift_defined % (nonlazy args,
  27.264 +                        (mk_trp((%%(dis_name c))`(con_app con args) ===
  27.265 +                              %%(if con=c then "TT" else "FF"))))) [
  27.266 +                                asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
  27.267 +        in flat(map (fn (c,_) => map (one_dis c) cons) cons) end;
  27.268    val dis_defins = map (fn (con,args) => pg [] (defined(%x_name) ==> 
  27.269 -		      defined(%%(dis_name con)`%x_name)) [
  27.270 -				rtac cases 1,
  27.271 -				contr_tac 1,
  27.272 -				UNTIL_SOLVED (CHANGED(asm_simp_tac 
  27.273 -				        (HOLCF_ss addsimps dis_apps) 1))]) cons;
  27.274 +                      defined(%%(dis_name con)`%x_name)) [
  27.275 +                                rtac cases 1,
  27.276 +                                contr_tac 1,
  27.277 +                                UNTIL_SOLVED (CHANGED(asm_simp_tac 
  27.278 +                                        (HOLCF_ss addsimps dis_apps) 1))]) cons;
  27.279  in dis_stricts @ dis_defins @ dis_apps end;
  27.280  
  27.281  val con_stricts = flat(map (fn (con,args) => map (fn vn =>
  27.282 -			pg (axs_con_def) 
  27.283 -			   (mk_trp(con_app2 con (fn arg => if vname arg = vn 
  27.284 -					then UU else %# arg) args === UU))[
  27.285 -				asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1]
  27.286 -			) (nonlazy args)) cons);
  27.287 +                        pg (axs_con_def) 
  27.288 +                           (mk_trp(con_app2 con (fn arg => if vname arg = vn 
  27.289 +                                        then UU else %# arg) args === UU))[
  27.290 +                                asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1]
  27.291 +                        ) (nonlazy args)) cons);
  27.292  val con_defins = map (fn (con,args) => pg []
  27.293 -			(lift_defined % (nonlazy args,
  27.294 -				mk_trp(defined(con_app con args)))) ([
  27.295 -			  rtac swap3 1, 
  27.296 -			  eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1,
  27.297 -			  asm_simp_tac (HOLCF_ss addsimps dis_rews) 1] )) cons;
  27.298 +                        (lift_defined % (nonlazy args,
  27.299 +                                mk_trp(defined(con_app con args)))) ([
  27.300 +                          rtac swap3 1, 
  27.301 +                          eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1,
  27.302 +                          asm_simp_tac (HOLCF_ss addsimps dis_rews) 1] )) cons;
  27.303  val con_rews = con_stricts @ con_defins;
  27.304  
  27.305  val sel_stricts = let fun one_sel sel = pg axs_sel_def (mk_trp(strict(%%sel))) [
  27.306 -				simp_tac (HOLCF_ss addsimps when_rews) 1];
  27.307 +                                simp_tac (HOLCF_ss addsimps when_rews) 1];
  27.308  in flat(map (fn (_,args) =>map (fn arg => one_sel (sel_of arg)) args) cons) end;
  27.309  val sel_apps = let fun one_sel c n sel = map (fn (con,args) => 
  27.310 -		let val nlas = nonlazy args;
  27.311 -		    val vns  = map vname args;
  27.312 -		in pg axs_sel_def (lift_defined %
  27.313 -		   (filter (fn v => con=c andalso (v<>nth_elem(n,vns))) nlas,
  27.314 -				mk_trp((%%sel)`(con_app con args) === 
  27.315 -				(if con=c then %(nth_elem(n,vns)) else UU))))
  27.316 -			    ( (if con=c then [] 
  27.317 -		       else map(case_UU_tac(when_rews@con_stricts)1) nlas)
  27.318 -		     @(if con=c andalso ((nth_elem(n,vns)) mem nlas)
  27.319 -				 then[case_UU_tac (when_rews @ con_stricts) 1 
  27.320 -						  (nth_elem(n,vns))] else [])
  27.321 -		     @ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons;
  27.322 +                let val nlas = nonlazy args;
  27.323 +                    val vns  = map vname args;
  27.324 +                in pg axs_sel_def (lift_defined %
  27.325 +                   (filter (fn v => con=c andalso (v<>nth_elem(n,vns))) nlas,
  27.326 +                                mk_trp((%%sel)`(con_app con args) === 
  27.327 +                                (if con=c then %(nth_elem(n,vns)) else UU))))
  27.328 +                            ( (if con=c then [] 
  27.329 +                       else map(case_UU_tac(when_rews@con_stricts)1) nlas)
  27.330 +                     @(if con=c andalso ((nth_elem(n,vns)) mem nlas)
  27.331 +                                 then[case_UU_tac (when_rews @ con_stricts) 1 
  27.332 +                                                  (nth_elem(n,vns))] else [])
  27.333 +                     @ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons;
  27.334  in flat(map  (fn (c,args) => 
  27.335       flat(mapn (fn n => fn arg => one_sel c n (sel_of arg)) 0 args)) cons) end;
  27.336  val sel_defins = if length cons=1 then map (fn arg => pg [](defined(%x_name)==> 
  27.337 -			defined(%%(sel_of arg)`%x_name)) [
  27.338 -				rtac cases 1,
  27.339 -				contr_tac 1,
  27.340 -				UNTIL_SOLVED (CHANGED(asm_simp_tac 
  27.341 -				             (HOLCF_ss addsimps sel_apps) 1))]) 
  27.342 -		 (filter_out is_lazy (snd(hd cons))) else [];
  27.343 +                        defined(%%(sel_of arg)`%x_name)) [
  27.344 +                                rtac cases 1,
  27.345 +                                contr_tac 1,
  27.346 +                                UNTIL_SOLVED (CHANGED(asm_simp_tac 
  27.347 +                                             (HOLCF_ss addsimps sel_apps) 1))]) 
  27.348 +                 (filter_out is_lazy (snd(hd cons))) else [];
  27.349  val sel_rews = sel_stricts @ sel_defins @ sel_apps;
  27.350  
  27.351  val distincts_le = let
  27.352      fun dist (con1, args1) (con2, args2) = pg []
  27.353 -	      (lift_defined % ((nonlazy args1),
  27.354 -			(mk_trp (con_app con1 args1 ~<< con_app con2 args2))))([
  27.355 -			rtac swap3 1,
  27.356 -			eres_inst_tac[("fo",dis_name con1)] monofun_cfun_arg 1]
  27.357 -		      @map(case_UU_tac (con_stricts @ dis_rews)1)(nonlazy args2)
  27.358 -		      @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]);
  27.359 +              (lift_defined % ((nonlazy args1),
  27.360 +                        (mk_trp (con_app con1 args1 ~<< con_app con2 args2))))([
  27.361 +                        rtac swap3 1,
  27.362 +                        eres_inst_tac[("fo",dis_name con1)] monofun_cfun_arg 1]
  27.363 +                      @map(case_UU_tac (con_stricts @ dis_rews)1)(nonlazy args2)
  27.364 +                      @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]);
  27.365      fun distinct (con1,args1) (con2,args2) =
  27.366 -	let val arg1 = (con1, args1);
  27.367 -	    val arg2 = (con2, (map (fn (arg,vn) => upd_vname (K vn) arg)
  27.368 -			(args2~~variantlist(map vname args2,map vname args1))));
  27.369 -	in [dist arg1 arg2, dist arg2 arg1] end;
  27.370 +        let val arg1 = (con1, args1);
  27.371 +            val arg2 = (con2, (map (fn (arg,vn) => upd_vname (K vn) arg)
  27.372 +                        (args2~~variantlist(map vname args2,map vname args1))));
  27.373 +        in [dist arg1 arg2, dist arg2 arg1] end;
  27.374      fun distincts []      = []
  27.375      |   distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
  27.376  in distincts cons end;
  27.377  val dists_le = flat (flat distincts_le);
  27.378  val dists_eq = let
  27.379      fun distinct (_,args1) ((_,args2),leqs) = let
  27.380 -	val (le1,le2) = (hd leqs, hd(tl leqs));
  27.381 -	val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) in
  27.382 -	if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
  27.383 -	if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
  27.384 -					[eq1, eq2] end;
  27.385 +        val (le1,le2) = (hd leqs, hd(tl leqs));
  27.386 +        val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) in
  27.387 +        if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
  27.388 +        if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
  27.389 +                                        [eq1, eq2] end;
  27.390      fun distincts []      = []
  27.391      |   distincts ((c,leqs)::cs) = flat(map (distinct c) ((map fst cs)~~leqs)) @
  27.392 -				   distincts cs;
  27.393 +                                   distincts cs;
  27.394      in distincts (cons~~distincts_le) end;
  27.395  
  27.396  local 
  27.397    fun pgterm rel con args = let
  27.398 -		fun append s = upd_vname(fn v => v^s);
  27.399 -		val (largs,rargs) = (args, map (append "'") args);
  27.400 -		in pg [] (mk_trp (rel(con_app con largs,con_app con rargs)) ===>
  27.401 -		      lift_defined % ((nonlazy largs),lift_defined % ((nonlazy rargs),
  27.402 -			    mk_trp (foldr' mk_conj 
  27.403 -				(map rel (map %# largs ~~ map %# rargs)))))) end;
  27.404 +                fun append s = upd_vname(fn v => v^s);
  27.405 +                val (largs,rargs) = (args, map (append "'") args);
  27.406 +                in pg [] (mk_trp (rel(con_app con largs,con_app con rargs)) ===>
  27.407 +                      lift_defined % ((nonlazy largs),lift_defined % ((nonlazy rargs),
  27.408 +                            mk_trp (foldr' mk_conj 
  27.409 +                                (map rel (map %# largs ~~ map %# rargs)))))) end;
  27.410    val cons' = filter (fn (_,args) => args<>[]) cons;
  27.411  in
  27.412  val inverts = map (fn (con,args) => 
  27.413 -		pgterm (op <<) con args (flat(map (fn arg => [
  27.414 -				TRY(rtac conjI 1),
  27.415 -				dres_inst_tac [("fo",sel_of arg)] monofun_cfun_arg 1,
  27.416 -				asm_full_simp_tac (HOLCF_ss addsimps sel_apps) 1]
  27.417 -			     			      ) args))) cons';
  27.418 +                pgterm (op <<) con args (flat(map (fn arg => [
  27.419 +                                TRY(rtac conjI 1),
  27.420 +                                dres_inst_tac [("fo",sel_of arg)] monofun_cfun_arg 1,
  27.421 +                                asm_full_simp_tac (HOLCF_ss addsimps sel_apps) 1]
  27.422 +                                                      ) args))) cons';
  27.423  val injects = map (fn ((con,args),inv_thm) => 
  27.424 -			   pgterm (op ===) con args [
  27.425 -				etac (antisym_less_inverse RS conjE) 1,
  27.426 -				dtac inv_thm 1, REPEAT(atac 1),
  27.427 -				dtac inv_thm 1, REPEAT(atac 1),
  27.428 -				TRY(safe_tac HOL_cs),
  27.429 -				REPEAT(rtac antisym_less 1 ORELSE atac 1)] )
  27.430 -		  (cons'~~inverts);
  27.431 +                           pgterm (op ===) con args [
  27.432 +                                etac (antisym_less_inverse RS conjE) 1,
  27.433 +                                dtac inv_thm 1, REPEAT(atac 1),
  27.434 +                                dtac inv_thm 1, REPEAT(atac 1),
  27.435 +                                TRY(safe_tac HOL_cs),
  27.436 +                                REPEAT(rtac antisym_less 1 ORELSE atac 1)] )
  27.437 +                  (cons'~~inverts);
  27.438  end;
  27.439  
  27.440  (* ----- theorems concerning one induction step ----------------------------- *)
  27.441  
  27.442  val copy_strict = pg[ax_copy_def](mk_trp(strict(dc_copy`%"f"))) [
  27.443 -		   asm_simp_tac(HOLCF_ss addsimps [abs_strict, when_strict,
  27.444 -						   cfst_strict,csnd_strict]) 1];
  27.445 +                   asm_simp_tac(HOLCF_ss addsimps [abs_strict, when_strict,
  27.446 +                                                   cfst_strict,csnd_strict]) 1];
  27.447  val copy_apps = map (fn (con,args) => pg [ax_copy_def]
  27.448 -		    (lift_defined % (nonlazy_rec args,
  27.449 -			mk_trp(dc_copy`%"f"`(con_app con args) ===
  27.450 -		(con_app2 con (app_rec_arg (cproj (%"f") (length eqs))) args))))
  27.451 -			(map (case_UU_tac (abs_strict::when_strict::con_stricts)
  27.452 -				 1 o vname)
  27.453 -			 (filter (fn a => not (is_rec a orelse is_lazy a)) args)
  27.454 -			@[asm_simp_tac (HOLCF_ss addsimps when_apps) 1,
  27.455 -		          simp_tac (HOLCF_ss addsimps axs_con_def) 1]))cons;
  27.456 +                    (lift_defined % (nonlazy_rec args,
  27.457 +                        mk_trp(dc_copy`%"f"`(con_app con args) ===
  27.458 +                (con_app2 con (app_rec_arg (cproj (%"f") (length eqs))) args))))
  27.459 +                        (map (case_UU_tac (abs_strict::when_strict::con_stricts)
  27.460 +                                 1 o vname)
  27.461 +                         (filter (fn a => not (is_rec a orelse is_lazy a)) args)
  27.462 +                        @[asm_simp_tac (HOLCF_ss addsimps when_apps) 1,
  27.463 +                          simp_tac (HOLCF_ss addsimps axs_con_def) 1]))cons;
  27.464  val copy_stricts = map (fn (con,args) => pg [] (mk_trp(dc_copy`UU`
  27.465 -					(con_app con args) ===UU))
  27.466 +                                        (con_app con args) ===UU))
  27.467       (let val rews = cfst_strict::csnd_strict::copy_strict::copy_apps@con_rews
  27.468 -			 in map (case_UU_tac rews 1) (nonlazy args) @ [
  27.469 -			     asm_simp_tac (HOLCF_ss addsimps rews) 1] end))
  27.470 -  		        (filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
  27.471 +                         in map (case_UU_tac rews 1) (nonlazy args) @ [
  27.472 +                             asm_simp_tac (HOLCF_ss addsimps rews) 1] end))
  27.473 +                        (filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
  27.474  val copy_rews = copy_strict::copy_apps @ copy_stricts;
  27.475  
  27.476  in     (iso_rews, exhaust, cases, when_rews,
  27.477 -	con_rews, sel_rews, dis_rews, dists_le, dists_eq, inverts, injects,
  27.478 -	copy_rews)
  27.479 +        con_rews, sel_rews, dis_rews, dists_le, dists_eq, inverts, injects,
  27.480 +        copy_rews)
  27.481  end; (* let *)
  27.482  
  27.483  
  27.484 @@ -377,68 +377,68 @@
  27.485  
  27.486  local
  27.487    val iterate_Cprod_ss = simpset_of "Fix"
  27.488 -			 addsimps [cfst_strict, csnd_strict]addsimps Cprod_rews;
  27.489 +                         addsimps [cfst_strict, csnd_strict]addsimps Cprod_rews;
  27.490    val copy_con_rews  = copy_rews @ con_rews;
  27.491    val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
  27.492    val take_stricts=pg copy_take_defs(mk_trp(foldr' mk_conj(map(fn((dn,args),_)=>
  27.493 -	    (dc_take dn $ %"n")`UU === mk_constrain(Type(dn,args),UU)) eqs)))([
  27.494 -			nat_ind_tac "n" 1,
  27.495 -			simp_tac iterate_Cprod_ss 1,
  27.496 -			asm_simp_tac (iterate_Cprod_ss addsimps copy_rews)1]);
  27.497 +            (dc_take dn $ %"n")`UU === mk_constrain(Type(dn,args),UU)) eqs)))([
  27.498 +                        nat_ind_tac "n" 1,
  27.499 +                        simp_tac iterate_Cprod_ss 1,
  27.500 +                        asm_simp_tac (iterate_Cprod_ss addsimps copy_rews)1]);
  27.501    val take_stricts' = rewrite_rule copy_take_defs take_stricts;
  27.502    val take_0s = mapn(fn n=> fn dn => pg axs_take_def(mk_trp((dc_take dn $ %%"0")
  27.503 -							`%x_name n === UU))[
  27.504 -				simp_tac iterate_Cprod_ss 1]) 1 dnames;
  27.505 +                                                        `%x_name n === UU))[
  27.506 +                                simp_tac iterate_Cprod_ss 1]) 1 dnames;
  27.507    val c_UU_tac = case_UU_tac (take_stricts'::copy_con_rews) 1;
  27.508    val take_apps = pg copy_take_defs (mk_trp(foldr' mk_conj 
  27.509 -	    (flat(map (fn ((dn,_),cons) => map (fn (con,args) => foldr mk_all 
  27.510 -	(map vname args,(dc_take dn $ (%%"Suc" $ %"n"))`(con_app con args) ===
  27.511 -  	 con_app2 con (app_rec_arg (fn n=>dc_take (nth_elem(n,dnames))$ %"n"))
  27.512 -			      args)) cons) eqs)))) ([
  27.513 -				simp_tac iterate_Cprod_ss 1,
  27.514 -				nat_ind_tac "n" 1,
  27.515 -			    simp_tac(iterate_Cprod_ss addsimps copy_con_rews) 1,
  27.516 -				asm_full_simp_tac (HOLCF_ss addsimps 
  27.517 -				      (filter (has_fewer_prems 1) copy_rews)) 1,
  27.518 -				TRY(safe_tac HOL_cs)] @
  27.519 -			(flat(map (fn ((dn,_),cons) => map (fn (con,args) => 
  27.520 -				if nonlazy_rec args = [] then all_tac else
  27.521 -				EVERY(map c_UU_tac (nonlazy_rec args)) THEN
  27.522 -				asm_full_simp_tac (HOLCF_ss addsimps copy_rews)1
  27.523 -		 					   ) cons) eqs)));
  27.524 +            (flat(map (fn ((dn,_),cons) => map (fn (con,args) => foldr mk_all 
  27.525 +        (map vname args,(dc_take dn $ (%%"Suc" $ %"n"))`(con_app con args) ===
  27.526 +         con_app2 con (app_rec_arg (fn n=>dc_take (nth_elem(n,dnames))$ %"n"))
  27.527 +                              args)) cons) eqs)))) ([
  27.528 +                                simp_tac iterate_Cprod_ss 1,
  27.529 +                                nat_ind_tac "n" 1,
  27.530 +                            simp_tac(iterate_Cprod_ss addsimps copy_con_rews) 1,
  27.531 +                                asm_full_simp_tac (HOLCF_ss addsimps 
  27.532 +                                      (filter (has_fewer_prems 1) copy_rews)) 1,
  27.533 +                                TRY(safe_tac HOL_cs)] @
  27.534 +                        (flat(map (fn ((dn,_),cons) => map (fn (con,args) => 
  27.535 +                                if nonlazy_rec args = [] then all_tac else
  27.536 +                                EVERY(map c_UU_tac (nonlazy_rec args)) THEN
  27.537 +                                asm_full_simp_tac (HOLCF_ss addsimps copy_rews)1
  27.538 +                                                           ) cons) eqs)));
  27.539  in
  27.540  val take_rews = atomize take_stricts @ take_0s @ atomize take_apps;
  27.541  end; (* local *)
  27.542  
  27.543  local
  27.544    fun one_con p (con,args) = foldr mk_All (map vname args,
  27.545 -	lift_defined (bound_arg (map vname args)) (nonlazy args,
  27.546 -	lift (fn arg => %(P_name (1+rec_of arg)) $ bound_arg args arg)
  27.547 +        lift_defined (bound_arg (map vname args)) (nonlazy args,
  27.548 +        lift (fn arg => %(P_name (1+rec_of arg)) $ bound_arg args arg)
  27.549           (filter is_rec args,mk_trp(%p $ con_app2 con (bound_arg args) args))));
  27.550    fun one_eq ((p,cons),concl) = (mk_trp(%p $ UU) ===> 
  27.551 -			   foldr (op ===>) (map (one_con p) cons,concl));
  27.552 +                           foldr (op ===>) (map (one_con p) cons,concl));
  27.553    fun ind_term concf = foldr one_eq (mapn (fn n => fn x => (P_name n, x))1conss,
  27.554 -			mk_trp(foldr' mk_conj (mapn concf 1 dnames)));
  27.555 +                        mk_trp(foldr' mk_conj (mapn concf 1 dnames)));
  27.556    val take_ss = HOL_ss addsimps take_rews;
  27.557    fun quant_tac i = EVERY(mapn(fn n=> fn _=> res_inst_tac[("x",x_name n)]spec i)
  27.558 -			       1 dnames);
  27.559 +                               1 dnames);
  27.560    fun ind_prems_tac prems = EVERY(flat (map (fn cons => (
  27.561 -				     resolve_tac prems 1 ::
  27.562 -				     flat (map (fn (_,args) => 
  27.563 -				       resolve_tac prems 1 ::
  27.564 -				       map (K(atac 1)) (nonlazy args) @
  27.565 -				       map (K(atac 1)) (filter is_rec args))
  27.566 -				     cons))) conss));
  27.567 +                                     resolve_tac prems 1 ::
  27.568 +                                     flat (map (fn (_,args) => 
  27.569 +                                       resolve_tac prems 1 ::
  27.570 +                                       map (K(atac 1)) (nonlazy args) @
  27.571 +                                       map (K(atac 1)) (filter is_rec args))
  27.572 +                                     cons))) conss));
  27.573    local 
  27.574      (* check whether every/exists constructor of the n-th part of the equation:
  27.575         it has a possibly indirectly recursive argument that isn't/is possibly 
  27.576         indirectly lazy *)
  27.577      fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg => 
  27.578 -	  is_rec arg andalso not(rec_of arg mem ns) andalso
  27.579 -	  ((rec_of arg =  n andalso nfn(lazy_rec orelse is_lazy arg)) orelse 
  27.580 -	    rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) 
  27.581 -	      (lazy_rec orelse is_lazy arg) (n, (nth_elem(rec_of arg,conss))))
  27.582 -	  ) o snd) cons;
  27.583 +          is_rec arg andalso not(rec_of arg mem ns) andalso
  27.584 +          ((rec_of arg =  n andalso nfn(lazy_rec orelse is_lazy arg)) orelse 
  27.585 +            rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) 
  27.586 +              (lazy_rec orelse is_lazy arg) (n, (nth_elem(rec_of arg,conss))))
  27.587 +          ) o snd) cons;
  27.588      fun all_rec_to ns  = rec_to forall not all_rec_to  ns;
  27.589      fun warn (n,cons)  = if all_rec_to [] false (n,cons) then (writeln 
  27.590          ("WARNING: domain "^nth_elem(n,dnames)^" is empty!"); true) else false;
  27.591 @@ -450,42 +450,42 @@
  27.592    end;
  27.593  in (* local *)
  27.594  val finite_ind = pg'' thy [] (ind_term (fn n => fn dn => %(P_name n)$
  27.595 -			     (dc_take dn $ %"n" `%(x_name n)))) (fn prems => [
  27.596 -				quant_tac 1,
  27.597 -				simp_tac quant_ss 1,
  27.598 -				nat_ind_tac "n" 1,
  27.599 -				simp_tac (take_ss addsimps prems) 1,
  27.600 -				TRY(safe_tac HOL_cs)]
  27.601 -				@ flat(map (fn (cons,cases) => [
  27.602 -				 res_inst_tac [("x","x")] cases 1,
  27.603 -				 asm_simp_tac (take_ss addsimps prems) 1]
  27.604 -				 @ flat(map (fn (con,args) => 
  27.605 -				  asm_simp_tac take_ss 1 ::
  27.606 -				  map (fn arg =>
  27.607 -				   case_UU_tac (prems@con_rews) 1 (
  27.608 -			   nth_elem(rec_of arg,dnames)^"_take n1`"^vname arg))
  27.609 -				  (filter is_nonlazy_rec args) @ [
  27.610 -				  resolve_tac prems 1] @
  27.611 -				  map (K (atac 1))      (nonlazy args) @
  27.612 -				  map (K (etac spec 1)) (filter is_rec args)) 
  27.613 -				 cons))
  27.614 -				(conss~~casess)));
  27.615 +                             (dc_take dn $ %"n" `%(x_name n)))) (fn prems => [
  27.616 +                                quant_tac 1,
  27.617 +                                simp_tac quant_ss 1,
  27.618 +                                nat_ind_tac "n" 1,
  27.619 +                                simp_tac (take_ss addsimps prems) 1,
  27.620 +                                TRY(safe_tac HOL_cs)]
  27.621 +                                @ flat(map (fn (cons,cases) => [
  27.622 +                                 res_inst_tac [("x","x")] cases 1,
  27.623 +                                 asm_simp_tac (take_ss addsimps prems) 1]
  27.624 +                                 @ flat(map (fn (con,args) => 
  27.625 +                                  asm_simp_tac take_ss 1 ::
  27.626 +                                  map (fn arg =>
  27.627 +                                   case_UU_tac (prems@con_rews) 1 (
  27.628 +                           nth_elem(rec_of arg,dnames)^"_take n1`"^vname arg))
  27.629 +                                  (filter is_nonlazy_rec args) @ [
  27.630 +                                  resolve_tac prems 1] @
  27.631 +                                  map (K (atac 1))      (nonlazy args) @
  27.632 +                                  map (K (etac spec 1)) (filter is_rec args)) 
  27.633 +                                 cons))
  27.634 +                                (conss~~casess)));
  27.635  
  27.636  val take_lemmas =mapn(fn n=> fn(dn,ax_reach)=> pg'' thy axs_take_def(mk_All("n",
  27.637 -		mk_trp(dc_take dn $ Bound 0 `%(x_name n) === 
  27.638 -		       dc_take dn $ Bound 0 `%(x_name n^"'")))
  27.639 -	   ===> mk_trp(%(x_name n) === %(x_name n^"'"))) (fn prems => [
  27.640 -			res_inst_tac[("t",x_name n    )](ax_reach RS subst) 1,
  27.641 -			res_inst_tac[("t",x_name n^"'")](ax_reach RS subst) 1,
  27.642 -				rtac (fix_def2 RS ssubst) 1,
  27.643 -				REPEAT(CHANGED(rtac(contlub_cfun_arg RS ssubst)1
  27.644 -					       THEN chain_tac 1)),
  27.645 -				rtac (contlub_cfun_fun RS ssubst) 1,
  27.646 -				rtac (contlub_cfun_fun RS ssubst) 2,
  27.647 -				rtac lub_equal 3,
  27.648 -				chain_tac 1,
  27.649 -				rtac allI 1,
  27.650 -				resolve_tac prems 1])) 1 (dnames~~axs_reach);
  27.651 +                mk_trp(dc_take dn $ Bound 0 `%(x_name n) === 
  27.652 +                       dc_take dn $ Bound 0 `%(x_name n^"'")))
  27.653 +           ===> mk_trp(%(x_name n) === %(x_name n^"'"))) (fn prems => [
  27.654 +                        res_inst_tac[("t",x_name n    )](ax_reach RS subst) 1,
  27.655 +                        res_inst_tac[("t",x_name n^"'")](ax_reach RS subst) 1,
  27.656 +                                stac fix_def2 1,
  27.657 +                                REPEAT(CHANGED(rtac(contlub_cfun_arg RS ssubst)1
  27.658 +                                               THEN chain_tac 1)),
  27.659 +                                stac contlub_cfun_fun 1,
  27.660 +                                stac contlub_cfun_fun 2,
  27.661 +                                rtac lub_equal 3,
  27.662 +                                chain_tac 1,
  27.663 +                                rtac allI 1,
  27.664 +                                resolve_tac prems 1])) 1 (dnames~~axs_reach);
  27.665  
  27.666  (* ----- theorems concerning finiteness and induction ----------------------- *)
  27.667  
  27.668 @@ -493,70 +493,70 @@
  27.669    let 
  27.670      fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %"x" === %"x");
  27.671      val finite_lemmas1a = map (fn dn => pg [] (mk_trp(defined (%"x")) ===> 
  27.672 -	mk_trp(mk_disj(mk_all("n",dc_take dn $ Bound 0 ` %"x" === UU),
  27.673 -	take_enough dn)) ===> mk_trp(take_enough dn)) [
  27.674 -				etac disjE 1,
  27.675 -				etac notE 1,
  27.676 -				resolve_tac take_lemmas 1,
  27.677 -				asm_simp_tac take_ss 1,
  27.678 -				atac 1]) dnames;
  27.679 +        mk_trp(mk_disj(mk_all("n",dc_take dn $ Bound 0 ` %"x" === UU),
  27.680 +        take_enough dn)) ===> mk_trp(take_enough dn)) [
  27.681 +                                etac disjE 1,
  27.682 +                                etac notE 1,
  27.683 +                                resolve_tac take_lemmas 1,
  27.684 +                                asm_simp_tac take_ss 1,
  27.685 +                                atac 1]) dnames;
  27.686      val finite_lemma1b = pg [] (mk_trp (mk_all("n",foldr' mk_conj (mapn 
  27.687 -	(fn n => fn ((dn,args),_) => mk_constrainall(x_name n,Type(dn,args),
  27.688 -	 mk_disj(dc_take dn $ Bound 1 ` Bound 0 === UU,
  27.689 -		 dc_take dn $ Bound 1 ` Bound 0 === Bound 0))) 1 eqs)))) ([
  27.690 -				rtac allI 1,
  27.691 -				nat_ind_tac "n" 1,
  27.692 -				simp_tac take_ss 1,
  27.693 -			TRY(safe_tac(empty_cs addSEs[conjE] addSIs[conjI]))] @
  27.694 -				flat(mapn (fn n => fn (cons,cases) => [
  27.695 -				  simp_tac take_ss 1,
  27.696 -				  rtac allI 1,
  27.697 -				  res_inst_tac [("x",x_name n)] cases 1,
  27.698 -				  asm_simp_tac take_ss 1] @ 
  27.699 -				  flat(map (fn (con,args) => 
  27.700 -				    asm_simp_tac take_ss 1 ::
  27.701 -				    flat(map (fn vn => [
  27.702 -				      eres_inst_tac [("x",vn)] all_dupE 1,
  27.703 -				      etac disjE 1,
  27.704 -				      asm_simp_tac (HOL_ss addsimps con_rews) 1,
  27.705 -				      asm_simp_tac take_ss 1])
  27.706 -				    (nonlazy_rec args)))
  27.707 -				  cons))
  27.708 -				1 (conss~~casess))) handle ERROR => raise ERROR;
  27.709 +        (fn n => fn ((dn,args),_) => mk_constrainall(x_name n,Type(dn,args),
  27.710 +         mk_disj(dc_take dn $ Bound 1 ` Bound 0 === UU,
  27.711 +                 dc_take dn $ Bound 1 ` Bound 0 === Bound 0))) 1 eqs)))) ([
  27.712 +                                rtac allI 1,
  27.713 +                                nat_ind_tac "n" 1,
  27.714 +                                simp_tac take_ss 1,
  27.715 +                        TRY(safe_tac(empty_cs addSEs[conjE] addSIs[conjI]))] @
  27.716 +                                flat(mapn (fn n => fn (cons,cases) => [
  27.717 +                                  simp_tac take_ss 1,
  27.718 +                                  rtac allI 1,
  27.719 +                                  res_inst_tac [("x",x_name n)] cases 1,
  27.720 +                                  asm_simp_tac take_ss 1] @ 
  27.721 +                                  flat(map (fn (con,args) => 
  27.722 +                                    asm_simp_tac take_ss 1 ::
  27.723 +                                    flat(map (fn vn => [
  27.724 +                                      eres_inst_tac [("x",vn)] all_dupE 1,
  27.725 +                                      etac disjE 1,
  27.726 +                                      asm_simp_tac (HOL_ss addsimps con_rews) 1,
  27.727 +                                      asm_simp_tac take_ss 1])
  27.728 +                                    (nonlazy_rec args)))
  27.729 +                                  cons))
  27.730 +                                1 (conss~~casess))) handle ERROR => raise ERROR;
  27.731      val finites = map (fn (dn,l1b) => pg axs_finite_def (mk_trp(
  27.732 -						%%(dn^"_finite") $ %"x"))[
  27.733 -				case_UU_tac take_rews 1 "x",
  27.734 -				eresolve_tac finite_lemmas1a 1,
  27.735 -				step_tac HOL_cs 1,
  27.736 -				step_tac HOL_cs 1,
  27.737 -				cut_facts_tac [l1b] 1,
  27.738 -			fast_tac HOL_cs 1]) (dnames~~atomize finite_lemma1b);
  27.739 +                                                %%(dn^"_finite") $ %"x"))[
  27.740 +                                case_UU_tac take_rews 1 "x",
  27.741 +                                eresolve_tac finite_lemmas1a 1,
  27.742 +                                step_tac HOL_cs 1,
  27.743 +                                step_tac HOL_cs 1,
  27.744 +                                cut_facts_tac [l1b] 1,
  27.745 +                        fast_tac HOL_cs 1]) (dnames~~atomize finite_lemma1b);
  27.746    in
  27.747    (finites,
  27.748     pg'' thy[](ind_term (fn n => fn dn => %(P_name n) $ %(x_name n)))(fn prems =>
  27.749 -				TRY(safe_tac HOL_cs) ::
  27.750 -			 flat (map (fn (finite,fin_ind) => [
  27.751 -			       rtac(rewrite_rule axs_finite_def finite RS exE)1,
  27.752 -				etac subst 1,
  27.753 -				rtac fin_ind 1,
  27.754 -				ind_prems_tac prems]) 
  27.755 -			           (finites~~(atomize finite_ind)) ))
  27.756 +                                TRY(safe_tac HOL_cs) ::
  27.757 +                         flat (map (fn (finite,fin_ind) => [
  27.758 +                               rtac(rewrite_rule axs_finite_def finite RS exE)1,
  27.759 +                                etac subst 1,
  27.760 +                                rtac fin_ind 1,
  27.761 +                                ind_prems_tac prems]) 
  27.762 +                                   (finites~~(atomize finite_ind)) ))
  27.763  ) end (* let *) else
  27.764    (mapn (fn n => fn dn => read_instantiate_sg (sign_of thy) 
  27.765 -	  	    [("P",dn^"_finite "^x_name n)] excluded_middle) 1 dnames,
  27.766 +                    [("P",dn^"_finite "^x_name n)] excluded_middle) 1 dnames,
  27.767     pg'' thy [] (foldr (op ===>) (mapn (fn n => K(mk_trp(%%"adm" $ %(P_name n))))
  27.768 -	       1 dnames, ind_term (fn n => fn dn => %(P_name n) $ %(x_name n))))
  27.769 -		   (fn prems => map (fn ax_reach => rtac (ax_reach RS subst) 1) 
  27.770 -				    axs_reach @ [
  27.771 -				quant_tac 1,
  27.772 -				rtac (adm_impl_admw RS wfix_ind) 1,
  27.773 -				REPEAT_DETERM(rtac adm_all2 1),
  27.774 -				REPEAT_DETERM(TRY(rtac adm_conj 1) THEN 
  27.775 -						  rtac adm_subst 1 THEN 
  27.776 -					cont_tacR 1 THEN resolve_tac prems 1),
  27.777 -				strip_tac 1,
  27.778 -				rtac (rewrite_rule axs_take_def finite_ind) 1,
  27.779 -				ind_prems_tac prems])
  27.780 +               1 dnames, ind_term (fn n => fn dn => %(P_name n) $ %(x_name n))))
  27.781 +                   (fn prems => map (fn ax_reach => rtac (ax_reach RS subst) 1) 
  27.782 +                                    axs_reach @ [
  27.783 +                                quant_tac 1,
  27.784 +                                rtac (adm_impl_admw RS wfix_ind) 1,
  27.785 +                                REPEAT_DETERM(rtac adm_all2 1),
  27.786 +                                REPEAT_DETERM(TRY(rtac adm_conj 1) THEN 
  27.787 +                                                  rtac adm_subst 1 THEN 
  27.788 +                                        cont_tacR 1 THEN resolve_tac prems 1),
  27.789 +                                strip_tac 1,
  27.790 +                                rtac (rewrite_rule axs_take_def finite_ind) 1,
  27.791 +                                ind_prems_tac prems])
  27.792  )
  27.793  end; (* local *)
  27.794  
  27.795 @@ -568,35 +568,35 @@
  27.796    val take_ss = HOL_ss addsimps take_rews;
  27.797    val sproj   = prj (fn s => "fst("^s^")") (fn s => "snd("^s^")");
  27.798    val coind_lemma=pg[ax_bisim_def](mk_trp(mk_imp(%%(comp_dname^"_bisim") $ %"R",
  27.799 -		foldr (fn (x,t)=> mk_all(x,mk_all(x^"'",t))) (xs,
  27.800 -		  foldr mk_imp (mapn (fn n => K(proj (%"R") n_eqs n $ 
  27.801 -				      bnd_arg n 0 $ bnd_arg n 1)) 0 dnames,
  27.802 -		    foldr' mk_conj (mapn (fn n => fn dn => 
  27.803 -				(dc_take dn $ %"n" `bnd_arg n 0 === 
  27.804 -				(dc_take dn $ %"n" `bnd_arg n 1)))0 dnames))))))
  27.805 -			     ([ rtac impI 1,
  27.806 -				nat_ind_tac "n" 1,
  27.807 -				simp_tac take_ss 1,
  27.808 -				safe_tac HOL_cs] @
  27.809 -				flat(mapn (fn n => fn x => [
  27.810 -				  rotate_tac (n+1) 1,
  27.811 -				  etac all2E 1,
  27.812 -				  eres_inst_tac [("P1", sproj "R" n_eqs n^
  27.813 -					" "^x^" "^x^"'")](mp RS disjE) 1,
  27.814 -				  TRY(safe_tac HOL_cs),
  27.815 -				  REPEAT(CHANGED(asm_simp_tac take_ss 1))]) 
  27.816 -				0 xs));
  27.817 +                foldr (fn (x,t)=> mk_all(x,mk_all(x^"'",t))) (xs,
  27.818 +                  foldr mk_imp (mapn (fn n => K(proj (%"R") n_eqs n $ 
  27.819 +                                      bnd_arg n 0 $ bnd_arg n 1)) 0 dnames,
  27.820 +                    foldr' mk_conj (mapn (fn n => fn dn => 
  27.821 +                                (dc_take dn $ %"n" `bnd_arg n 0 === 
  27.822 +                                (dc_take dn $ %"n" `bnd_arg n 1)))0 dnames))))))
  27.823 +                             ([ rtac impI 1,
  27.824 +                                nat_ind_tac "n" 1,
  27.825 +                                simp_tac take_ss 1,
  27.826 +                                safe_tac HOL_cs] @
  27.827 +                                flat(mapn (fn n => fn x => [
  27.828 +                                  rotate_tac (n+1) 1,
  27.829 +                                  etac all2E 1,
  27.830 +                                  eres_inst_tac [("P1", sproj "R" n_eqs n^
  27.831 +                                        " "^x^" "^x^"'")](mp RS disjE) 1,
  27.832 +                                  TRY(safe_tac HOL_cs),
  27.833 +                                  REPEAT(CHANGED(asm_simp_tac take_ss 1))]) 
  27.834 +                                0 xs));
  27.835  in
  27.836  val coind = pg [] (mk_trp(%%(comp_dname^"_bisim") $ %"R") ===>
  27.837 -		foldr (op ===>) (mapn (fn n => fn x => 
  27.838 -		  mk_trp(proj (%"R") n_eqs n $ %x $ %(x^"'"))) 0 xs,
  27.839 -		  mk_trp(foldr' mk_conj (map (fn x => %x === %(x^"'")) xs)))) ([
  27.840 -				TRY(safe_tac HOL_cs)] @
  27.841 -				flat(map (fn take_lemma => [
  27.842 -				  rtac take_lemma 1,
  27.843 -				  cut_facts_tac [coind_lemma] 1,
  27.844 -				  fast_tac HOL_cs 1])
  27.845 -				take_lemmas));
  27.846 +                foldr (op ===>) (mapn (fn n => fn x => 
  27.847 +                  mk_trp(proj (%"R") n_eqs n $ %x $ %(x^"'"))) 0 xs,
  27.848 +                  mk_trp(foldr' mk_conj (map (fn x => %x === %(x^"'")) xs)))) ([
  27.849 +                                TRY(safe_tac HOL_cs)] @
  27.850 +                                flat(map (fn take_lemma => [
  27.851 +                                  rtac take_lemma 1,
  27.852 +                                  cut_facts_tac [coind_lemma] 1,
  27.853 +                                  fast_tac HOL_cs 1])
  27.854 +                                take_lemmas));
  27.855  end; (* local *)
  27.856  
  27.857  
    28.1 --- a/src/HOLCF/ex/Hoare.ML	Thu Sep 26 12:50:48 1996 +0200
    28.2 +++ b/src/HOLCF/ex/Hoare.ML	Thu Sep 26 15:14:23 1996 +0200
    28.3 @@ -179,7 +179,7 @@
    28.4          (simp_tac HOLCF_ss 1),
    28.5          (etac mp 1),
    28.6          (strip_tac 1),
    28.7 -	(fast_tac (HOL_cs addSDs [less_Suc_eq RS iffD1]) 1)]);
    28.8 +        (fast_tac (HOL_cs addSDs [less_Suc_eq RS iffD1]) 1)]);
    28.9  
   28.10  (* -------- results about p for case (? k. b1`(iterate k g x)~=TT) ------- *)
   28.11  
   28.12 @@ -275,14 +275,14 @@
   28.13   (fn prems =>
   28.14          [
   28.15          (cut_facts_tac prems 1),
   28.16 -        (rtac (p_def2 RS ssubst) 1),
   28.17 +        (stac p_def2 1),
   28.18          (rtac fix_ind 1),
   28.19          (rtac adm_all 1),
   28.20          (rtac allI 1),
   28.21          (rtac adm_eq 1),
   28.22          (cont_tacR 1),
   28.23          (rtac allI 1),
   28.24 -        (rtac (strict_fapp1 RS ssubst) 1),
   28.25 +        (stac strict_fapp1 1),
   28.26          (rtac refl 1),
   28.27          (Simp_tac 1),
   28.28          (rtac allI 1),
   28.29 @@ -309,14 +309,14 @@
   28.30   (fn prems =>
   28.31          [
   28.32          (cut_facts_tac prems 1),
   28.33 -        (rtac (q_def2 RS ssubst) 1),
   28.34 +        (stac q_def2 1),
   28.35          (rtac fix_ind 1),
   28.36          (rtac adm_all 1),
   28.37          (rtac allI 1),
   28.38          (rtac adm_eq 1),
   28.39          (cont_tacR 1),
   28.40          (rtac allI 1),
   28.41 -        (rtac (strict_fapp1 RS ssubst) 1),
   28.42 +        (stac strict_fapp1 1),
   28.43          (rtac refl 1),
   28.44          (rtac allI 1),
   28.45          (Simp_tac 1),
   28.46 @@ -351,14 +351,14 @@
   28.47   (fn prems =>
   28.48          [
   28.49          (cut_facts_tac prems 1),
   28.50 -        (rtac (q_def2 RS ssubst) 1),
   28.51 +        (stac q_def2 1),
   28.52          (rtac fix_ind 1),
   28.53          (rtac adm_all 1),
   28.54          (rtac allI 1),
   28.55          (rtac adm_eq 1),
   28.56          (cont_tacR 1),
   28.57          (rtac allI 1),
   28.58 -        (rtac (strict_fapp1 RS ssubst) 1),
   28.59 +        (stac strict_fapp1 1),
   28.60          (rtac refl 1),
   28.61          (rtac allI 1),
   28.62          (Simp_tac 1),
   28.63 @@ -383,7 +383,7 @@
   28.64   (fn prems =>
   28.65          [
   28.66          (cut_facts_tac prems 1),
   28.67 -        (rtac (q_def3 RS ssubst) 1),
   28.68 +        (stac q_def3 1),
   28.69          (asm_simp_tac HOLCF_ss 1)
   28.70          ]);
   28.71  
   28.72 @@ -437,7 +437,7 @@
   28.73          (Simp_tac 1),
   28.74          (strip_tac 1),
   28.75          (etac conjE 1),
   28.76 -        (rtac (q_def3 RS ssubst) 1),
   28.77 +        (stac q_def3 1),
   28.78          (asm_simp_tac HOLCF_ss 1),
   28.79          (hyp_subst_tac 1),
   28.80          (Simp_tac 1),
   28.81 @@ -467,18 +467,18 @@
   28.82   (fn prems =>
   28.83          [
   28.84          (cut_facts_tac prems 1),
   28.85 -        (rtac (hoare_lemma16 RS ssubst) 1),
   28.86 +        (stac hoare_lemma16 1),
   28.87          (atac 1),
   28.88          (rtac (hoare_lemma19 RS disjE) 1),
   28.89          (atac 1),
   28.90 -        (rtac (hoare_lemma18 RS ssubst) 1),
   28.91 +        (stac hoare_lemma18 1),
   28.92          (atac 1),
   28.93 -        (rtac (hoare_lemma22 RS ssubst) 1),
   28.94 +        (stac hoare_lemma22 1),
   28.95          (atac 1),
   28.96          (rtac refl 1),
   28.97 -        (rtac (hoare_lemma21 RS ssubst) 1),
   28.98 +        (stac hoare_lemma21 1),
   28.99          (atac 1),
  28.100 -        (rtac (hoare_lemma21 RS ssubst) 1),
  28.101 +        (stac hoare_lemma21 1),
  28.102          (atac 1),
  28.103          (rtac refl 1)
  28.104          ]);
  28.105 @@ -493,7 +493,7 @@
  28.106          (rtac (hoare_lemma5 RS disjE) 1),
  28.107          (atac 1),
  28.108          (rtac refl 1),
  28.109 -        (rtac (hoare_lemma11 RS mp RS ssubst) 1),
  28.110 +        (stac (hoare_lemma11 RS mp) 1),
  28.111          (atac 1),
  28.112          (rtac conjI 1),
  28.113          (rtac refl 1),
  28.114 @@ -504,17 +504,17 @@
  28.115          (rtac refl 1),
  28.116          (atac 1),
  28.117          (rtac refl 1),
  28.118 -        (rtac (hoare_lemma12 RS mp RS ssubst) 1),
  28.119 +        (stac (hoare_lemma12 RS mp) 1),
  28.120          (atac 1),
  28.121          (rtac conjI 1),
  28.122          (rtac refl 1),
  28.123          (atac 1),
  28.124 -        (rtac (hoare_lemma22 RS ssubst) 1),
  28.125 -        (rtac (hoare_lemma28 RS ssubst) 1),
  28.126 +        (stac hoare_lemma22 1),
  28.127 +        (stac hoare_lemma28 1),
  28.128          (atac 1),
  28.129          (rtac refl 1),
  28.130          (rtac sym 1),
  28.131 -        (rtac (hoare_lemma27 RS mp RS ssubst) 1),
  28.132 +        (stac (hoare_lemma27 RS mp) 1),
  28.133          (atac 1),
  28.134          (rtac conjI 1),
  28.135          (rtac refl 1),
  28.136 @@ -528,7 +528,7 @@
  28.137   (fn prems =>
  28.138          [
  28.139          (rtac ext_cfun 1),
  28.140 -        (rtac (cfcomp2 RS ssubst) 1),
  28.141 +        (stac cfcomp2 1),
  28.142          (rtac (hoare_lemma3 RS disjE) 1),
  28.143          (etac hoare_lemma23 1),
  28.144          (etac hoare_lemma29 1)
    29.1 --- a/src/HOLCF/ex/Loop.ML	Thu Sep 26 12:50:48 1996 +0200
    29.2 +++ b/src/HOLCF/ex/Loop.ML	Thu Sep 26 15:14:23 1996 +0200
    29.3 @@ -47,15 +47,15 @@
    29.4          (simp_tac HOLCF_ss 1),
    29.5          (rtac allI 1),
    29.6          (rtac trans 1),
    29.7 -        (rtac (while_unfold RS ssubst) 1),
    29.8 +        (stac while_unfold 1),
    29.9          (rtac refl 2),
   29.10 -        (rtac (iterate_Suc2 RS ssubst) 1),
   29.11 +        (stac iterate_Suc2 1),
   29.12          (rtac trans 1),
   29.13          (etac spec 2),
   29.14 -        (rtac (step_def2 RS ssubst) 1),
   29.15 +        (stac step_def2 1),
   29.16          (res_inst_tac [("p","b`x")] trE 1),
   29.17          (asm_simp_tac HOLCF_ss 1),
   29.18 -        (rtac (while_unfold RS ssubst) 1),
   29.19 +        (stac while_unfold 1),
   29.20          (res_inst_tac [("s","UU"),("t","b`UU")]ssubst 1),
   29.21          (etac (flat_tr RS flat_codom RS disjE) 1),
   29.22          (atac 1),
   29.23 @@ -63,7 +63,7 @@
   29.24          (simp_tac HOLCF_ss 1),
   29.25          (asm_simp_tac HOLCF_ss 1),
   29.26          (asm_simp_tac HOLCF_ss 1),
   29.27 -        (rtac (while_unfold RS ssubst) 1),
   29.28 +        (stac while_unfold 1),
   29.29          (asm_simp_tac HOLCF_ss 1)
   29.30          ]);
   29.31  
   29.32 @@ -144,10 +144,10 @@
   29.33          (nat_ind_tac "k" 1),
   29.34          (Simp_tac 1),
   29.35          (strip_tac 1),
   29.36 -        (rtac (while_unfold RS ssubst) 1),
   29.37 +        (stac while_unfold 1),
   29.38          (asm_simp_tac HOLCF_ss 1),
   29.39          (rtac allI 1),
   29.40 -        (rtac (iterate_Suc2 RS ssubst) 1),
   29.41 +        (stac iterate_Suc2 1),
   29.42          (strip_tac 1),
   29.43          (rtac trans 1),
   29.44          (rtac while_unfold3 1),
   29.45 @@ -160,7 +160,7 @@
   29.46   (fn prems =>
   29.47          [
   29.48          (cut_facts_tac prems 1),
   29.49 -        (rtac (while_def2 RS ssubst) 1),
   29.50 +        (stac while_def2 1),
   29.51          (rtac fix_ind 1),
   29.52          (rtac (allI RS adm_all) 1),
   29.53          (rtac adm_eq 1),
   29.54 @@ -224,7 +224,7 @@
   29.55          (res_inst_tac [("P","%k. b`(iterate k (step`b`g) x)=FF")] exE 1),
   29.56          (rtac loop_lemma7 1),
   29.57          (resolve_tac prems 1),
   29.58 -        (rtac ((loop_lemma4 RS spec RS mp) RS ssubst) 1),
   29.59 +        (stac (loop_lemma4 RS spec RS mp) 1),
   29.60          (atac 1),
   29.61          (rtac (nth_elem (1,prems) RS spec RS mp) 1),
   29.62          (rtac conjI 1),
    30.1 --- a/src/HOLCF/ex/loeckx.ML	Thu Sep 26 12:50:48 1996 +0200
    30.2 +++ b/src/HOLCF/ex/loeckx.ML	Thu Sep 26 15:14:23 1996 +0200
    30.3 @@ -4,7 +4,7 @@
    30.4  
    30.5  val prems = goalw Fix.thy [Ifix_def]
    30.6  "Ifix F= lub (range (%i.%G.iterate i G UU)) F";
    30.7 -by (rtac (thelub_fun RS ssubst) 1);
    30.8 +by (stac thelub_fun 1);
    30.9  by (rtac ch2ch_fun 1);
   30.10  back();
   30.11  by (rtac refl 2);
   30.12 @@ -59,7 +59,7 @@
   30.13          "(% i.iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)" 1);
   30.14  by (etac arg_cong 1);
   30.15  by (rtac ext 1);
   30.16 -by (rtac (beta_cfun RS ssubst) 1);
   30.17 +by (stac beta_cfun 1);
   30.18  by (rtac  cont2cont_CF1L 1);
   30.19  by (rtac cont_iterate 1);
   30.20  by (rtac refl 1);
   30.21 @@ -67,10 +67,10 @@
   30.22  by (rtac is_chainI 1);
   30.23  by (strip_tac 1);
   30.24  by (rtac less_cfun2 1);
   30.25 -by (rtac (beta_cfun RS ssubst) 1);
   30.26 +by (stac beta_cfun 1);
   30.27  by (rtac  cont2cont_CF1L 1);
   30.28  by (rtac cont_iterate 1);
   30.29 -by (rtac (beta_cfun RS ssubst) 1);
   30.30 +by (stac beta_cfun 1);
   30.31  by (rtac  cont2cont_CF1L 1);
   30.32  by (rtac cont_iterate 1);
   30.33  by (rtac (is_chain_iterate RS is_chainE RS spec) 1);
   30.34 @@ -81,7 +81,7 @@
   30.35  val prems = goal Fix.thy  
   30.36  "(% i.iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)";
   30.37  by (rtac ext 1);
   30.38 -by (rtac (beta_cfun RS ssubst) 1);
   30.39 +by (stac beta_cfun 1);
   30.40  by (rtac  cont2cont_CF1L 1);
   30.41  by (rtac cont_iterate 1);
   30.42  by (rtac refl 1);
   30.43 @@ -91,7 +91,7 @@
   30.44  " Ifix = (%f.lub(range(%j.(LAM f.iterate j f UU)`f)))";
   30.45  by (rtac ext 1);
   30.46  by (rewtac Ifix_def ); 
   30.47 -by (rtac (fix_lemma1 RS ssubst) 1);
   30.48 +by (stac fix_lemma1 1);
   30.49  by (rtac refl 1);
   30.50  val fix_lemma2 = result();
   30.51  
   30.52 @@ -102,15 +102,15 @@
   30.53  *)
   30.54  
   30.55  val prems = goal Fix.thy "cont Ifix";
   30.56 -by (rtac ( fix_lemma2  RS ssubst) 1);
   30.57 +by (stac fix_lemma2 1);
   30.58  by (rtac cont_lubcfun 1);
   30.59  by (rtac is_chainI 1);
   30.60  by (strip_tac 1);
   30.61  by (rtac less_cfun2 1);
   30.62 -by (rtac (beta_cfun RS ssubst) 1);
   30.63 +by (stac beta_cfun 1);
   30.64  by (rtac  cont2cont_CF1L 1);
   30.65  by (rtac cont_iterate 1);
   30.66 -by (rtac (beta_cfun RS ssubst) 1);
   30.67 +by (stac beta_cfun 1);
   30.68  by (rtac  cont2cont_CF1L 1);
   30.69  by (rtac cont_iterate 1);
   30.70  by (rtac (is_chain_iterate RS is_chainE RS spec) 1);
    31.1 --- a/src/HOLCF/explicit_domains/Coind.ML	Thu Sep 26 12:50:48 1996 +0200
    31.2 +++ b/src/HOLCF/explicit_domains/Coind.ML	Thu Sep 26 15:14:23 1996 +0200
    31.3 @@ -28,7 +28,7 @@
    31.4   (fn prems =>
    31.5          [
    31.6          (rtac trans 1),
    31.7 -        (rtac (from_def2 RS ssubst) 1),
    31.8 +        (stac from_def2 1),
    31.9          (Simp_tac 1),
   31.10          (rtac refl 1)
   31.11          ]);
   31.12 @@ -38,7 +38,7 @@
   31.13   (fn prems =>
   31.14          [
   31.15          (rtac trans 1),
   31.16 -        (rtac (from RS ssubst) 1),
   31.17 +        (stac from 1),
   31.18          (resolve_tac  stream_constrdef 1),
   31.19          (rtac refl 1)
   31.20          ]);
   31.21 @@ -119,17 +119,17 @@
   31.22          (etac conjE 1),
   31.23          (hyp_subst_tac 1),
   31.24          (rtac conjI 1),
   31.25 -        (rtac (coind_lemma1 RS ssubst) 1),
   31.26 -        (rtac (from RS ssubst) 1),
   31.27 +        (stac coind_lemma1 1),
   31.28 +        (stac from 1),
   31.29          (asm_simp_tac (!simpset addsimps stream_rews) 1),
   31.30          (res_inst_tac [("x","dsucc`n")] exI 1),
   31.31          (rtac conjI 1),
   31.32          (rtac trans 1),
   31.33 -        (rtac (coind_lemma1 RS ssubst) 1),
   31.34 +        (stac coind_lemma1 1),
   31.35          (asm_simp_tac (!simpset addsimps stream_rews) 1),
   31.36          (rtac refl 1),
   31.37          (rtac trans 1),
   31.38 -        (rtac (from RS ssubst) 1),
   31.39 +        (stac from 1),
   31.40          (asm_simp_tac (!simpset addsimps stream_rews) 1),
   31.41          (rtac refl 1),
   31.42          (res_inst_tac [("x","dzero")] exI 1),
    32.1 --- a/src/HOLCF/explicit_domains/Dagstuhl.ML	Thu Sep 26 12:50:48 1996 +0200
    32.2 +++ b/src/HOLCF/explicit_domains/Dagstuhl.ML	Thu Sep 26 15:14:23 1996 +0200
    32.3 @@ -12,7 +12,7 @@
    32.4  by (resolve_tac adm_thms 1);
    32.5  by (cont_tacR 1);
    32.6  by (rtac minimal 1);
    32.7 -by (rtac (beta_cfun RS ssubst) 1);
    32.8 +by (stac beta_cfun 1);
    32.9  by (cont_tacR 1);
   32.10  by (rtac monofun_cfun_arg 1);
   32.11  by (rtac monofun_cfun_arg 1);
   32.12 @@ -20,7 +20,7 @@
   32.13  val lemma3 = result();
   32.14  
   32.15  val prems = goal Dagstuhl.thy "scons`y`YYS << YYS";
   32.16 -by (rtac (YYS_def2 RS ssubst) 1);
   32.17 +by (stac YYS_def2 1);
   32.18  back();
   32.19  by (rtac monofun_cfun_arg 1);
   32.20  by (rtac lemma3 1);
   32.21 @@ -38,8 +38,8 @@
   32.22  by (rtac stream_take_lemma 1);
   32.23  by (nat_ind_tac "n" 1);
   32.24  by (simp_tac (!simpset addsimps stream_rews) 1);
   32.25 -by (rtac (YS_def2 RS ssubst) 1);
   32.26 -by (rtac (YYS_def2 RS ssubst) 1);
   32.27 +by (stac YS_def2 1);
   32.28 +by (stac YYS_def2 1);
   32.29  by (asm_simp_tac (!simpset addsimps stream_rews) 1);
   32.30  by (rtac (lemma5 RS sym RS subst) 1);
   32.31  by (rtac refl 1);
   32.32 @@ -54,7 +54,7 @@
   32.33  val prems = goal Dagstuhl.thy "YYS << YS";
   32.34  by (rewtac YYS_def);
   32.35  by (rtac fix_least 1);
   32.36 -by (rtac (beta_cfun RS ssubst) 1);
   32.37 +by (stac beta_cfun 1);
   32.38  by (cont_tacR 1);
   32.39  by (simp_tac (!simpset addsimps [YS_def2 RS sym]) 1);
   32.40  val lemma6=result();
   32.41 @@ -65,9 +65,9 @@
   32.42  by (resolve_tac adm_thms 1);
   32.43  by (cont_tacR 1);
   32.44  by (rtac minimal 1);
   32.45 -by (rtac (beta_cfun RS ssubst) 1);
   32.46 +by (stac beta_cfun 1);
   32.47  by (cont_tacR 1);
   32.48 -by (rtac (lemma5 RS sym RS ssubst) 1);
   32.49 +by (stac (lemma5 RS sym) 1);
   32.50  by (etac monofun_cfun_arg 1);
   32.51  val lemma7 = result();
   32.52  
    33.1 --- a/src/HOLCF/explicit_domains/Dlist.ML	Thu Sep 26 12:50:48 1996 +0200
    33.2 +++ b/src/HOLCF/explicit_domains/Dlist.ML	Thu Sep 26 15:14:23 1996 +0200
    33.3 @@ -427,10 +427,10 @@
    33.4          [
    33.5          (res_inst_tac [("t","l1")] (reach RS subst) 1),
    33.6          (res_inst_tac [("t","l2")] (reach RS subst) 1),
    33.7 -        (rtac (fix_def2 RS ssubst) 1),
    33.8 -        (rtac (contlub_cfun_fun RS ssubst) 1),
    33.9 +        (stac fix_def2 1),
   33.10 +        (stac contlub_cfun_fun 1),
   33.11          (rtac is_chain_iterate 1),
   33.12 -        (rtac (contlub_cfun_fun RS ssubst) 1),
   33.13 +        (stac contlub_cfun_fun 1),
   33.14          (rtac is_chain_iterate 1),
   33.15          (rtac lub_equal 1),
   33.16          (rtac (is_chain_iterate RS ch2ch_fappL) 1),
    34.1 --- a/src/HOLCF/explicit_domains/Dnat.ML	Thu Sep 26 12:50:48 1996 +0200
    34.2 +++ b/src/HOLCF/explicit_domains/Dnat.ML	Thu Sep 26 15:14:23 1996 +0200
    34.3 @@ -339,10 +339,10 @@
    34.4          [
    34.5          (res_inst_tac [("t","s1")] (reach RS subst) 1),
    34.6          (res_inst_tac [("t","s2")] (reach RS subst) 1),
    34.7 -        (rtac (fix_def2 RS ssubst) 1),
    34.8 -        (rtac (contlub_cfun_fun RS ssubst) 1),
    34.9 +        (stac fix_def2 1),
   34.10 +        (stac contlub_cfun_fun 1),
   34.11          (rtac is_chain_iterate 1),
   34.12 -        (rtac (contlub_cfun_fun RS ssubst) 1),
   34.13 +        (stac contlub_cfun_fun 1),
   34.14          (rtac is_chain_iterate 1),
   34.15          (rtac lub_equal 1),
   34.16          (rtac (is_chain_iterate RS ch2ch_fappL) 1),
    35.1 --- a/src/HOLCF/explicit_domains/Dnat2.ML	Thu Sep 26 12:50:48 1996 +0200
    35.2 +++ b/src/HOLCF/explicit_domains/Dnat2.ML	Thu Sep 26 15:14:23 1996 +0200
    35.3 @@ -23,14 +23,14 @@
    35.4  qed_goal "iterator1" Dnat2.thy "iterator`UU`f`x = UU"
    35.5   (fn prems =>
    35.6          [
    35.7 -        (rtac (iterator_def2 RS ssubst) 1),
    35.8 +        (stac iterator_def2 1),
    35.9          (simp_tac (!simpset addsimps dnat_when) 1)
   35.10          ]);
   35.11  
   35.12  qed_goal "iterator2" Dnat2.thy "iterator`dzero`f`x = x"
   35.13   (fn prems =>
   35.14          [
   35.15 -        (rtac (iterator_def2 RS ssubst) 1),
   35.16 +        (stac iterator_def2 1),
   35.17          (simp_tac (!simpset addsimps dnat_when) 1)
   35.18          ]);
   35.19  
   35.20 @@ -40,7 +40,7 @@
   35.21          [
   35.22          (cut_facts_tac prems 1),
   35.23          (rtac trans 1),
   35.24 -        (rtac (iterator_def2 RS ssubst) 1),
   35.25 +        (stac iterator_def2 1),
   35.26          (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   35.27          (rtac refl 1)
   35.28          ]);
    36.1 --- a/src/HOLCF/explicit_domains/Stream.ML	Thu Sep 26 12:50:48 1996 +0200
    36.2 +++ b/src/HOLCF/explicit_domains/Stream.ML	Thu Sep 26 15:14:23 1996 +0200
    36.3 @@ -311,20 +311,20 @@
    36.4  
    36.5  fun prover reach defs thm  = prove_goalw Stream.thy defs thm
    36.6   (fn prems =>
    36.7 -	[
    36.8 -	(res_inst_tac [("t","s1")] (reach RS subst) 1),
    36.9 -	(res_inst_tac [("t","s2")] (reach RS subst) 1),
   36.10 -	(rtac (fix_def2 RS ssubst) 1),
   36.11 -	(rtac (contlub_cfun_fun RS ssubst) 1),
   36.12 -	(rtac is_chain_iterate 1),
   36.13 -	(rtac (contlub_cfun_fun RS ssubst) 1),
   36.14 -	(rtac is_chain_iterate 1),
   36.15 -	(rtac lub_equal 1),
   36.16 -	(rtac (is_chain_iterate RS ch2ch_fappL) 1),
   36.17 -	(rtac (is_chain_iterate RS ch2ch_fappL) 1),
   36.18 -	(rtac allI 1),
   36.19 -	(resolve_tac prems 1),
   36.20 -	]);
   36.21 +        [
   36.22 +        (res_inst_tac [("t","s1")] (reach RS subst) 1),
   36.23 +        (res_inst_tac [("t","s2")] (reach RS subst) 1),
   36.24 +        (stac fix_def2 1),
   36.25 +        (stac contlub_cfun_fun 1),
   36.26 +        (rtac is_chain_iterate 1),
   36.27 +        (stac contlub_cfun_fun 1),
   36.28 +        (rtac is_chain_iterate 1),
   36.29 +        (rtac lub_equal 1),
   36.30 +        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
   36.31 +        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
   36.32 +        (rtac allI 1),
   36.33 +        (resolve_tac prems 1),
   36.34 +        ]);
   36.35  
   36.36  val stream_take_lemma = prover stream_reach  [stream_take_def]
   36.37          "(!!n.stream_take n`s1 = stream_take n`s2) ==> s1=s2";
   36.38 @@ -334,9 +334,9 @@
   36.39   (fn prems =>
   36.40          [
   36.41          (res_inst_tac [("t","s")] (stream_reach RS subst) 1),
   36.42 -        (rtac (fix_def2 RS ssubst) 1),
   36.43 +        (stac fix_def2 1),
   36.44          (rewtac stream_take_def),
   36.45 -        (rtac (contlub_cfun_fun RS ssubst) 1),
   36.46 +        (stac contlub_cfun_fun 1),
   36.47          (rtac is_chain_iterate 1),
   36.48          (rtac refl 1)
   36.49          ]);
   36.50 @@ -640,9 +640,9 @@
   36.51          (strip_tac 1),
   36.52          (res_inst_tac [("s","s")] streamE 1),
   36.53          (hyp_subst_tac 1),
   36.54 -        (rtac (iterate_Suc2 RS ssubst) 1),
   36.55 +        (stac iterate_Suc2 1),
   36.56          (asm_simp_tac (!simpset addsimps stream_rews) 1),
   36.57 -        (rtac (iterate_Suc2 RS ssubst) 1),
   36.58 +        (stac iterate_Suc2 1),
   36.59          (asm_simp_tac (!simpset addsimps stream_rews) 1),
   36.60          (etac allE 1),
   36.61          (etac mp 1),
   36.62 @@ -664,7 +664,7 @@
   36.63          (hyp_subst_tac 1),
   36.64          (asm_simp_tac (!simpset addsimps stream_rews) 1),
   36.65          (hyp_subst_tac 1),
   36.66 -        (rtac (iterate_Suc2 RS ssubst) 1),
   36.67 +        (stac iterate_Suc2 1),
   36.68          (asm_simp_tac (!simpset addsimps stream_rews) 1)
   36.69          ]);
   36.70  
   36.71 @@ -833,7 +833,7 @@
   36.72          (REPEAT(resolve_tac adm_thms 1)),
   36.73          (rtac  cont_iterate2 1),
   36.74          (rtac allI 1),
   36.75 -        (rtac (stream_finite_lemma8 RS ssubst) 1),
   36.76 +        (stac stream_finite_lemma8 1),
   36.77          (fast_tac HOL_cs 1)
   36.78          ]);
   36.79  
    37.1 --- a/src/HOLCF/explicit_domains/Stream2.ML	Thu Sep 26 12:50:48 1996 +0200
    37.2 +++ b/src/HOLCF/explicit_domains/Stream2.ML	Thu Sep 26 15:14:23 1996 +0200
    37.3 @@ -24,7 +24,7 @@
    37.4  qed_goal "smap1" Stream2.thy "smap`f`UU = UU"
    37.5   (fn prems =>
    37.6          [
    37.7 -        (rtac (smap_def2 RS ssubst) 1),
    37.8 +        (stac smap_def2 1),
    37.9          (simp_tac (!simpset addsimps stream_when) 1)
   37.10          ]);
   37.11  
   37.12 @@ -34,7 +34,7 @@
   37.13          [
   37.14          (cut_facts_tac prems 1),
   37.15          (rtac trans 1),
   37.16 -        (rtac (smap_def2 RS ssubst) 1),
   37.17 +        (stac smap_def2 1),
   37.18          (asm_simp_tac (!simpset addsimps stream_rews) 1),
   37.19          (rtac refl 1)
   37.20          ]);
    38.1 --- a/src/ZF/Arith.ML	Thu Sep 26 12:50:48 1996 +0200
    38.2 +++ b/src/ZF/Arith.ML	Thu Sep 26 15:14:23 1996 +0200
    38.3 @@ -450,7 +450,7 @@
    38.4  qed "add_le_self";
    38.5  
    38.6  goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m le n #+ m";
    38.7 -by (rtac (add_commute RS ssubst) 1);
    38.8 +by (stac add_commute 1);
    38.9  by (REPEAT (ares_tac [add_le_self] 1));
   38.10  qed "add_le_self2";
   38.11  
   38.12 @@ -468,8 +468,8 @@
   38.13  goal Arith.thy "!!i j k l. [| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
   38.14  by (rtac (add_lt_mono1 RS lt_trans) 1);
   38.15  by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
   38.16 -by (EVERY [rtac (add_commute RS ssubst) 1,
   38.17 -           rtac (add_commute RS ssubst) 3,
   38.18 +by (EVERY [stac add_commute 1,
   38.19 +           stac add_commute 3,
   38.20             rtac add_lt_mono1 5]);
   38.21  by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
   38.22  qed "add_lt_mono";
   38.23 @@ -496,8 +496,8 @@
   38.24      "!!i j k. [| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l";
   38.25  by (rtac (add_le_mono1 RS le_trans) 1);
   38.26  by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
   38.27 -by (EVERY [rtac (add_commute RS ssubst) 1,
   38.28 -           rtac (add_commute RS ssubst) 3,
   38.29 +by (EVERY [stac add_commute 1,
   38.30 +           stac add_commute 3,
   38.31             rtac add_le_mono1 5]);
   38.32  by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
   38.33  qed "add_le_mono";
   38.34 @@ -516,8 +516,8 @@
   38.35      "!!i j k. [| i le j; k le l; j:nat; l:nat |] ==> i#*k le j#*l";
   38.36  by (rtac (mult_le_mono1 RS le_trans) 1);
   38.37  by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
   38.38 -by (EVERY [rtac (mult_commute RS ssubst) 1,
   38.39 -           rtac (mult_commute RS ssubst) 3,
   38.40 +by (EVERY [stac mult_commute 1,
   38.41 +           stac mult_commute 3,
   38.42             rtac mult_le_mono1 5]);
   38.43  by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
   38.44  qed "mult_le_mono";
    39.1 --- a/src/ZF/Cardinal.ML	Thu Sep 26 12:50:48 1996 +0200
    39.2 +++ b/src/ZF/Cardinal.ML	Thu Sep 26 15:14:23 1996 +0200
    39.3 @@ -200,7 +200,7 @@
    39.4  by (trans_ind_tac "i" [] 1);
    39.5  by (rtac impI 1);
    39.6  by (rtac classical 1);
    39.7 -by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]);
    39.8 +by (EVERY1 [stac Least_equality, assume_tac, assume_tac]);
    39.9  by (assume_tac 2);
   39.10  by (fast_tac (ZF_cs addSEs [ltE]) 1);
   39.11  qed "LeastI";
   39.12 @@ -211,7 +211,7 @@
   39.13  by (trans_ind_tac "i" [] 1);
   39.14  by (rtac impI 1);
   39.15  by (rtac classical 1);
   39.16 -by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]);
   39.17 +by (EVERY1 [stac Least_equality, assume_tac, assume_tac]);
   39.18  by (etac le_refl 2);
   39.19  by (fast_tac (ZF_cs addEs [ltE, lt_trans1] addIs [leI, ltI]) 1);
   39.20  qed "Least_le";
   39.21 @@ -299,7 +299,7 @@
   39.22  (* Could replace the  ~(j eqpoll i)  by  ~(i lepoll j) *)
   39.23  val prems = goalw Cardinal.thy [Card_def,cardinal_def]
   39.24      "[| Ord(i);  !!j. j<i ==> ~(j eqpoll i) |] ==> Card(i)";
   39.25 -by (rtac (Least_equality RS ssubst) 1);
   39.26 +by (stac Least_equality 1);
   39.27  by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1));
   39.28  qed "CardI";
   39.29  
   39.30 @@ -481,7 +481,7 @@
   39.31  (*The object of all this work: every natural number is a (finite) cardinal*)
   39.32  goalw Cardinal.thy [Card_def,cardinal_def]
   39.33      "!!n. n: nat ==> Card(n)";
   39.34 -by (rtac (Least_equality RS ssubst) 1);
   39.35 +by (stac Least_equality 1);
   39.36  by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl]));
   39.37  by (asm_simp_tac (ZF_ss addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1);
   39.38  by (fast_tac (ZF_cs addSEs [lt_irrefl]) 1);
   39.39 @@ -549,7 +549,7 @@
   39.40  qed "Ord_nat_eqpoll_iff";
   39.41  
   39.42  goalw Cardinal.thy [Card_def,cardinal_def] "Card(nat)";
   39.43 -by (rtac (Least_equality RS ssubst) 1);
   39.44 +by (stac Least_equality 1);
   39.45  by (REPEAT_FIRST (ares_tac [eqpoll_refl, Ord_nat, refl]));
   39.46  by (etac ltE 1);
   39.47  by (asm_simp_tac (ZF_ss addsimps [eqpoll_iff, lt_not_lepoll, ltI]) 1);
    40.1 --- a/src/ZF/Cardinal_AC.ML	Thu Sep 26 12:50:48 1996 +0200
    40.2 +++ b/src/ZF/Cardinal_AC.ML	Thu Sep 26 15:14:23 1996 +0200
    40.3 @@ -34,7 +34,7 @@
    40.4      "!!A. [| |A|=|B|;  |C|=|D|;  A Int C = 0;  B Int D = 0 |] ==> \
    40.5  \         |A Un C| = |B Un D|";
    40.6  by (asm_full_simp_tac (ZF_ss addsimps [cardinal_eqpoll_iff, 
    40.7 -				       eqpoll_disjoint_Un]) 1);
    40.8 +                                       eqpoll_disjoint_Un]) 1);
    40.9  qed "cardinal_disjoint_Un";
   40.10  
   40.11  goal Cardinal_AC.thy "!!A B. A lepoll B ==> |A| le |B|";
    41.1 --- a/src/ZF/Epsilon.ML	Thu Sep 26 12:50:48 1996 +0200
    41.2 +++ b/src/ZF/Epsilon.ML	Thu Sep 26 15:14:23 1996 +0200
    41.3 @@ -154,7 +154,7 @@
    41.4      "[| !!x u. [| x:eclose({a});  u: Pi(x,B) |] ==> H(x,u) : B(x)   \
    41.5  \    |]  ==> transrec(a,H) : B(a)";
    41.6  by (res_inst_tac [("i", "a")] (arg_in_eclose_sing RS eclose_induct) 1);
    41.7 -by (rtac (transrec RS ssubst) 1);
    41.8 +by (stac transrec 1);
    41.9  by (REPEAT (ares_tac (prems @ [lam_type]) 1 ORELSE etac bspec 1));
   41.10  qed "transrec_type";
   41.11  
   41.12 @@ -177,13 +177,13 @@
   41.13  
   41.14  (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
   41.15  goal Epsilon.thy "rank(a) = (UN y:a. succ(rank(y)))";
   41.16 -by (rtac (rank_def RS def_transrec RS ssubst) 1);
   41.17 +by (stac (rank_def RS def_transrec) 1);
   41.18  by (simp_tac ZF_ss 1);
   41.19  qed "rank";
   41.20  
   41.21  goal Epsilon.thy "Ord(rank(a))";
   41.22  by (eps_ind_tac "a" 1);
   41.23 -by (rtac (rank RS ssubst) 1);
   41.24 +by (stac rank 1);
   41.25  by (rtac (Ord_succ RS Ord_UN) 1);
   41.26  by (etac bspec 1);
   41.27  by (assume_tac 1);
   41.28 @@ -191,7 +191,7 @@
   41.29  
   41.30  val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
   41.31  by (rtac (major RS trans_induct) 1);
   41.32 -by (rtac (rank RS ssubst) 1);
   41.33 +by (stac rank 1);
   41.34  by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1);
   41.35  qed "rank_of_Ord";
   41.36  
   41.37 @@ -211,8 +211,8 @@
   41.38  
   41.39  goal Epsilon.thy "!!a b. a<=b ==> rank(a) le rank(b)";
   41.40  by (rtac subset_imp_le 1);
   41.41 -by (rtac (rank RS ssubst) 1);
   41.42 -by (rtac (rank RS ssubst) 1);
   41.43 +by (stac rank 1);
   41.44 +by (stac rank 1);
   41.45  by (etac UN_mono 1);
   41.46  by (REPEAT (resolve_tac [subset_refl, Ord_rank] 1));
   41.47  qed "rank_mono";
   41.48 @@ -243,7 +243,7 @@
   41.49  by (rtac equalityI 1);
   41.50  by (rtac (rank_mono RS le_imp_subset RS UN_least) 2);
   41.51  by (etac Union_upper 2);
   41.52 -by (rtac (rank RS ssubst) 1);
   41.53 +by (stac rank 1);
   41.54  by (rtac UN_least 1);
   41.55  by (etac UnionE 1);
   41.56  by (rtac subset_trans 1);
    42.1 --- a/src/ZF/Finite.ML	Thu Sep 26 12:50:48 1996 +0200
    42.2 +++ b/src/ZF/Finite.ML	Thu Sep 26 15:14:23 1996 +0200
    42.3 @@ -73,7 +73,7 @@
    42.4  \       !!x y. [| x: A;  y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
    42.5  \    |] ==> c<=b --> P(b-c)";
    42.6  by (rtac (major RS Fin_induct) 1);
    42.7 -by (rtac (Diff_cons RS ssubst) 2);
    42.8 +by (stac Diff_cons 2);
    42.9  by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff, 
   42.10                                  Diff_subset RS Fin_subset]))));
   42.11  qed "Fin_0_induct_lemma";
    43.1 --- a/src/ZF/List.ML	Thu Sep 26 12:50:48 1996 +0200
    43.2 +++ b/src/ZF/List.ML	Thu Sep 26 15:14:23 1996 +0200
    43.3 @@ -110,8 +110,8 @@
    43.4      "!!i. i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
    43.5  by (etac nat_induct 1);
    43.6  by (simp_tac (nat_ss addsimps [tl_Cons]) 1);
    43.7 -by (rtac (rec_succ RS ssubst) 1);
    43.8 -by (rtac (rec_succ RS ssubst) 1);
    43.9 +by (stac rec_succ 1);
   43.10 +by (stac rec_succ 1);
   43.11  by (asm_simp_tac ZF_ss 1);
   43.12  qed "drop_succ_Cons";
   43.13  
   43.14 @@ -219,7 +219,7 @@
   43.15  
   43.16  goalw List.thy [set_of_list_def] 
   43.17      "!!l. l: list(A) ==> set_of_list(l) : Pow(A)";
   43.18 -be list_rec_type 1;
   43.19 +by (etac list_rec_type 1);
   43.20  by (ALLGOALS (fast_tac ZF_cs));
   43.21  qed "set_of_list_type";
   43.22  
   43.23 @@ -228,7 +228,7 @@
   43.24  \         set_of_list (xs@ys) = set_of_list(xs) Un set_of_list(ys)";
   43.25  by (etac list.induct 1);
   43.26  by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [set_of_list_Nil,set_of_list_Cons,
   43.27 -					    app_Nil,app_Cons,Un_cons])));
   43.28 +                                            app_Nil,app_Cons,Un_cons])));
   43.29  qed "set_of_list_append";
   43.30  
   43.31  
    44.1 --- a/src/ZF/Nat.ML	Thu Sep 26 12:50:48 1996 +0200
    44.2 +++ b/src/ZF/Nat.ML	Thu Sep 26 15:14:23 1996 +0200
    44.3 @@ -21,12 +21,12 @@
    44.4  (** Type checking of 0 and successor **)
    44.5  
    44.6  goal Nat.thy "0 : nat";
    44.7 -by (rtac (nat_unfold RS ssubst) 1);
    44.8 +by (stac nat_unfold 1);
    44.9  by (rtac (singletonI RS UnI1) 1);
   44.10  qed "nat_0I";
   44.11  
   44.12  val prems = goal Nat.thy "n : nat ==> succ(n) : nat";
   44.13 -by (rtac (nat_unfold RS ssubst) 1);
   44.14 +by (stac nat_unfold 1);
   44.15  by (rtac (RepFunI RS UnI2) 1);
   44.16  by (resolve_tac prems 1);
   44.17  qed "nat_succI";
    45.1 --- a/src/ZF/OrderType.ML	Thu Sep 26 12:50:48 1996 +0200
    45.2 +++ b/src/ZF/OrderType.ML	Thu Sep 26 15:14:23 1996 +0200
    45.3 @@ -116,7 +116,7 @@
    45.4  
    45.5  goalw OrderType.thy [ordertype_def]
    45.6      "!!r. well_ord(A,r) ==> Ord(ordertype(A,r))";
    45.7 -by (rtac ([ordermap_type, subset_refl] MRS image_fun RS ssubst) 1);
    45.8 +by (stac ([ordermap_type, subset_refl] MRS image_fun) 1);
    45.9  by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
   45.10  by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2);
   45.11  by (rewrite_goals_tac [Transset_def,well_ord_def]);
    46.1 --- a/src/ZF/Ordinal.ML	Thu Sep 26 12:50:48 1996 +0200
    46.2 +++ b/src/ZF/Ordinal.ML	Thu Sep 26 15:14:23 1996 +0200
    46.3 @@ -532,7 +532,7 @@
    46.4  (*Replacing k by succ(k') yields the similar rule for le!*)
    46.5  goal Ordinal.thy "!!i j k. [| i<k;  j<k |] ==> i Un j < k";
    46.6  by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1);
    46.7 -by (rtac (Un_commute RS ssubst) 4);
    46.8 +by (stac Un_commute 4);
    46.9  by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Un_iff]) 4);
   46.10  by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Un_iff]) 3);
   46.11  by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
   46.12 @@ -555,7 +555,7 @@
   46.13  (*Replacing k by succ(k') yields the similar rule for le!*)
   46.14  goal Ordinal.thy "!!i j k. [| i<k;  j<k |] ==> i Int j < k";
   46.15  by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1);
   46.16 -by (rtac (Int_commute RS ssubst) 4);
   46.17 +by (stac Int_commute 4);
   46.18  by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Int_iff]) 4);
   46.19  by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Int_iff]) 3);
   46.20  by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
    47.1 --- a/src/ZF/Perm.ML	Thu Sep 26 12:50:48 1996 +0200
    47.2 +++ b/src/ZF/Perm.ML	Thu Sep 26 15:14:23 1996 +0200
    47.3 @@ -157,7 +157,7 @@
    47.4  
    47.5  goalw Perm.thy [inj_def] "!!f. f: inj(A,B) ==> converse(f) : range(f)->A";
    47.6  by (asm_simp_tac (ZF_ss addsimps [Pi_iff, function_def]) 1);
    47.7 -by (eresolve_tac [CollectE] 1);
    47.8 +by (etac CollectE 1);
    47.9  by (asm_simp_tac (ZF_ss addsimps [apply_iff]) 1);
   47.10  by (fast_tac (ZF_cs addDs [fun_is_rel]) 1);
   47.11  qed "inj_converse_fun";
   47.12 @@ -192,7 +192,7 @@
   47.13  
   47.14  goal Perm.thy "!!f. [| f: bij(A,B);  b: B |] ==> f`(converse(f)`b) = b";
   47.15  by (fast_tac (ZF_cs addss
   47.16 -	      (ZF_ss addsimps [bij_def, right_inverse, surj_range])) 1);
   47.17 +              (ZF_ss addsimps [bij_def, right_inverse, surj_range])) 1);
   47.18  qed "right_inverse_bij";
   47.19  
   47.20  (** Converses of injections, surjections, bijections **)
   47.21 @@ -207,12 +207,12 @@
   47.22  goal Perm.thy "!!f A B. f: inj(A,B) ==> converse(f): surj(range(f), A)";
   47.23  by (ITER_DEEPEN (has_fewer_prems 1)
   47.24      (ares_tac [f_imp_surjective, inj_converse_fun, left_inverse,
   47.25 -	       inj_is_fun, range_of_fun RS apply_type]));
   47.26 +               inj_is_fun, range_of_fun RS apply_type]));
   47.27  qed "inj_converse_surj";
   47.28  
   47.29  goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> converse(f): bij(B,A)";
   47.30  by (fast_tac (ZF_cs addEs [surj_range RS subst, inj_converse_inj,
   47.31 -			   inj_converse_surj]) 1);
   47.32 +                           inj_converse_surj]) 1);
   47.33  qed "bij_converse_bij";
   47.34  
   47.35  
   47.36 @@ -307,7 +307,7 @@
   47.37  by (asm_full_simp_tac
   47.38      (ZF_ss addsimps [Pi_def, comp_function, Pow_iff, comp_rel]
   47.39             setloop etac conjE) 1);
   47.40 -by (rtac (range_rel_subset RS domain_comp_eq RS ssubst) 1 THEN assume_tac 2);
   47.41 +by (stac (range_rel_subset RS domain_comp_eq) 1 THEN assume_tac 2);
   47.42  by (fast_tac ZF_cs 1);
   47.43  qed "comp_fun";
   47.44  
   47.45 @@ -470,7 +470,7 @@
   47.46      "!!f g. [| f: bij(A,B);  g: bij(C,D);  A Int C = 0;  B Int D = 0 |] ==> \
   47.47  \           (f Un g) : bij(A Un C, B Un D)";
   47.48  by (rtac invertible_imp_bijective 1);
   47.49 -by (rtac (converse_Un RS ssubst) 1);
   47.50 +by (stac converse_Un 1);
   47.51  by (REPEAT (ares_tac [fun_disjoint_Un, bij_is_fun, bij_converse_bij] 1));
   47.52  qed "bij_disjoint_Un";
   47.53  
   47.54 @@ -533,7 +533,7 @@
   47.55      "!!f. [| f: inj(A,B);  a~:A;  b~:B |]  ==> \
   47.56  \         cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
   47.57  by (fast_tac (ZF_cs  addIs [apply_type]
   47.58 -	             addss (ZF_ss addsimps [fun_extend, fun_extend_apply2,
   47.59 -					    fun_extend_apply1]) ) 1);
   47.60 +                     addss (ZF_ss addsimps [fun_extend, fun_extend_apply2,
   47.61 +                                            fun_extend_apply1]) ) 1);
   47.62  qed "inj_extend";
   47.63  
    48.1 --- a/src/ZF/QUniv.ML	Thu Sep 26 12:50:48 1996 +0200
    48.2 +++ b/src/ZF/QUniv.ML	Thu Sep 26 15:14:23 1996 +0200
    48.3 @@ -19,7 +19,7 @@
    48.4  
    48.5  val [prem] = goalw QUniv.thy [sum_def]
    48.6      "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
    48.7 -by (rtac (Int_Un_distrib RS ssubst) 1);
    48.8 +by (stac Int_Un_distrib 1);
    48.9  by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1);
   48.10  qed "Transset_sum_Int_subset";
   48.11  
   48.12 @@ -201,7 +201,7 @@
   48.13  goalw QUniv.thy [QPair_def,sum_def]
   48.14   "!!X. Transset(X) ==>          \
   48.15  \      <a;b> Int Vfrom(X, succ(i))  <=  <a Int Vfrom(X,i);  b Int Vfrom(X,i)>";
   48.16 -by (rtac (Int_Un_distrib RS ssubst) 1);
   48.17 +by (stac Int_Un_distrib 1);
   48.18  by (rtac Un_mono 1);
   48.19  by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans,
   48.20                        [Int_lower1, subset_refl] MRS Sigma_mono] 1));
   48.21 @@ -226,7 +226,7 @@
   48.22  \      |] ==> <a;b> Int Vset(i)  <=  (UN j:i. <a Int Vset(j); b Int Vset(j)>)";
   48.23  by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
   48.24  (*0 case*)
   48.25 -by (rtac (Vfrom_0 RS ssubst) 1);
   48.26 +by (stac Vfrom_0 1);
   48.27  by (fast_tac ZF_cs 1);
   48.28  (*succ(j) case*)
   48.29  by (rtac (Transset_0 RS QPair_Int_Vfrom_succ_subset RS subset_trans) 1);
    49.1 --- a/src/ZF/Univ.ML	Thu Sep 26 12:50:48 1996 +0200
    49.2 +++ b/src/ZF/Univ.ML	Thu Sep 26 15:14:23 1996 +0200
    49.3 @@ -10,7 +10,7 @@
    49.4  
    49.5  (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
    49.6  goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
    49.7 -by (rtac (Vfrom_def RS def_transrec RS ssubst) 1);
    49.8 +by (stac (Vfrom_def RS def_transrec) 1);
    49.9  by (simp_tac ZF_ss 1);
   49.10  qed "Vfrom";
   49.11  
   49.12 @@ -19,8 +19,8 @@
   49.13  goal Univ.thy "!!A B. A<=B ==> ALL j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)";
   49.14  by (eps_ind_tac "i" 1);
   49.15  by (rtac (impI RS allI) 1);
   49.16 -by (rtac (Vfrom RS ssubst) 1);
   49.17 -by (rtac (Vfrom RS ssubst) 1);
   49.18 +by (stac Vfrom 1);
   49.19 +by (stac Vfrom 1);
   49.20  by (etac Un_mono 1);
   49.21  by (rtac UN_mono 1);
   49.22  by (assume_tac 1);
   49.23 @@ -38,15 +38,15 @@
   49.24  
   49.25  goal Univ.thy "Vfrom(A,x) <= Vfrom(A,rank(x))";
   49.26  by (eps_ind_tac "x" 1);
   49.27 -by (rtac (Vfrom RS ssubst) 1);
   49.28 -by (rtac (Vfrom RS ssubst) 1);
   49.29 +by (stac Vfrom 1);
   49.30 +by (stac Vfrom 1);
   49.31  by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1);
   49.32  qed "Vfrom_rank_subset1";
   49.33  
   49.34  goal Univ.thy "Vfrom(A,rank(x)) <= Vfrom(A,x)";
   49.35  by (eps_ind_tac "x" 1);
   49.36 -by (rtac (Vfrom RS ssubst) 1);
   49.37 -by (rtac (Vfrom RS ssubst) 1);
   49.38 +by (stac Vfrom 1);
   49.39 +by (stac Vfrom 1);
   49.40  by (rtac (subset_refl RS Un_mono) 1);
   49.41  by (rtac UN_least 1);
   49.42  (*expand rank(x1) = (UN y:x1. succ(rank(y))) in assumptions*)
   49.43 @@ -70,25 +70,25 @@
   49.44  (*** Basic closure properties ***)
   49.45  
   49.46  goal Univ.thy "!!x y. y:x ==> 0 : Vfrom(A,x)";
   49.47 -by (rtac (Vfrom RS ssubst) 1);
   49.48 +by (stac Vfrom 1);
   49.49  by (fast_tac ZF_cs 1);
   49.50  qed "zero_in_Vfrom";
   49.51  
   49.52  goal Univ.thy "i <= Vfrom(A,i)";
   49.53  by (eps_ind_tac "i" 1);
   49.54 -by (rtac (Vfrom RS ssubst) 1);
   49.55 +by (stac Vfrom 1);
   49.56  by (fast_tac ZF_cs 1);
   49.57  qed "i_subset_Vfrom";
   49.58  
   49.59  goal Univ.thy "A <= Vfrom(A,i)";
   49.60 -by (rtac (Vfrom RS ssubst) 1);
   49.61 +by (stac Vfrom 1);
   49.62  by (rtac Un_upper1 1);
   49.63  qed "A_subset_Vfrom";
   49.64  
   49.65  bind_thm ("A_into_Vfrom", A_subset_Vfrom RS subsetD);
   49.66  
   49.67  goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))";
   49.68 -by (rtac (Vfrom RS ssubst) 1);
   49.69 +by (stac Vfrom 1);
   49.70  by (fast_tac ZF_cs 1);
   49.71  qed "subset_mem_Vfrom";
   49.72  
   49.73 @@ -121,7 +121,7 @@
   49.74  (*** 0, successor and limit equations fof Vfrom ***)
   49.75  
   49.76  goal Univ.thy "Vfrom(A,0) = A";
   49.77 -by (rtac (Vfrom RS ssubst) 1);
   49.78 +by (stac Vfrom 1);
   49.79  by (fast_tac eq_cs 1);
   49.80  qed "Vfrom_0";
   49.81  
   49.82 @@ -138,14 +138,14 @@
   49.83  goal Univ.thy "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
   49.84  by (res_inst_tac [("x1", "succ(i)")] (Vfrom_rank_eq RS subst) 1);
   49.85  by (res_inst_tac [("x1", "i")] (Vfrom_rank_eq RS subst) 1);
   49.86 -by (rtac (rank_succ RS ssubst) 1);
   49.87 +by (stac rank_succ 1);
   49.88  by (rtac (Ord_rank RS Vfrom_succ_lemma) 1);
   49.89  qed "Vfrom_succ";
   49.90  
   49.91  (*The premise distinguishes this from Vfrom(A,0);  allowing X=0 forces
   49.92    the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *)
   49.93  val [prem] = goal Univ.thy "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
   49.94 -by (rtac (Vfrom RS ssubst) 1);
   49.95 +by (stac Vfrom 1);
   49.96  by (rtac equalityI 1);
   49.97  (*first inclusion*)
   49.98  by (rtac Un_least 1);
   49.99 @@ -155,11 +155,11 @@
  49.100  by (etac UnionE 1);
  49.101  by (rtac subset_trans 1);
  49.102  by (etac UN_upper 2);
  49.103 -by (rtac (Vfrom RS ssubst) 1);
  49.104 +by (stac Vfrom 1);
  49.105  by (etac ([UN_upper, Un_upper2] MRS subset_trans) 1);
  49.106  (*opposite inclusion*)
  49.107  by (rtac UN_least 1);
  49.108 -by (rtac (Vfrom RS ssubst) 1);
  49.109 +by (stac Vfrom 1);
  49.110  by (fast_tac ZF_cs 1);
  49.111  qed "Vfrom_Union";
  49.112  
  49.113 @@ -170,7 +170,7 @@
  49.114  val [limiti] = goal Univ.thy
  49.115      "Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))";
  49.116  by (rtac (limiti RS (Limit_has_0 RS ltD) RS Vfrom_Union RS subst) 1);
  49.117 -by (rtac (limiti RS Limit_Union_eq RS ssubst) 1);
  49.118 +by (stac (limiti RS Limit_Union_eq) 1);
  49.119  by (rtac refl 1);
  49.120  qed "Limit_Vfrom_eq";
  49.121  
  49.122 @@ -269,7 +269,7 @@
  49.123  
  49.124  goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))";
  49.125  by (eps_ind_tac "i" 1);
  49.126 -by (rtac (Vfrom RS ssubst) 1);
  49.127 +by (stac Vfrom 1);
  49.128  by (fast_tac (ZF_cs addSIs [Transset_Union_family, Transset_Un,
  49.129                              Transset_Pow]) 1);
  49.130  qed "Transset_Vfrom";
  49.131 @@ -365,7 +365,7 @@
  49.132  by (dtac Transset_Vfrom 1);
  49.133  by (rtac subset_mem_Vfrom 1);
  49.134  by (rtac (Collect_subset RS subset_trans) 1);
  49.135 -by (rtac (Vfrom RS ssubst) 1);
  49.136 +by (stac Vfrom 1);
  49.137  by (rtac (subset_trans RS subset_trans) 1);
  49.138  by (rtac Un_upper2 3);
  49.139  by (rtac (succI1 RS UN_upper) 2);
  49.140 @@ -386,7 +386,7 @@
  49.141  (*** The set Vset(i) ***)
  49.142  
  49.143  goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))";
  49.144 -by (rtac (Vfrom RS ssubst) 1);
  49.145 +by (stac Vfrom 1);
  49.146  by (fast_tac eq_cs 1);
  49.147  qed "Vset";
  49.148  
  49.149 @@ -398,9 +398,9 @@
  49.150  
  49.151  val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i";
  49.152  by (rtac (ordi RS trans_induct) 1);
  49.153 -by (rtac (Vset RS ssubst) 1);
  49.154 +by (stac Vset 1);
  49.155  by (safe_tac ZF_cs);
  49.156 -by (rtac (rank RS ssubst) 1);
  49.157 +by (stac rank 1);
  49.158  by (rtac UN_succ_least_lt 1);
  49.159  by (fast_tac ZF_cs 2);
  49.160  by (REPEAT (ares_tac [ltI] 1));
  49.161 @@ -412,7 +412,7 @@
  49.162  val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
  49.163  by (rtac (ordi RS trans_induct) 1);
  49.164  by (rtac allI 1);
  49.165 -by (rtac (Vset RS ssubst) 1);
  49.166 +by (stac Vset 1);
  49.167  by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1);
  49.168  qed "Vset_rank_imp2";
  49.169  
  49.170 @@ -433,7 +433,7 @@
  49.171  qed "Vset_rank_iff";
  49.172  
  49.173  goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i";
  49.174 -by (rtac (rank RS ssubst) 1);
  49.175 +by (stac rank 1);
  49.176  by (rtac equalityI 1);
  49.177  by (safe_tac ZF_cs);
  49.178  by (EVERY' [rtac UN_I, 
  49.179 @@ -471,7 +471,7 @@
  49.180  
  49.181  (*NOT SUITABLE FOR REWRITING: recursive!*)
  49.182  goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
  49.183 -by (rtac (transrec RS ssubst) 1);
  49.184 +by (stac transrec 1);
  49.185  by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta, 
  49.186                                VsetI RS beta, le_refl]) 1);
  49.187  qed "Vrec";
  49.188 @@ -511,7 +511,7 @@
  49.189      "[| a <= univ(X);                           \
  49.190  \       !!i. i:nat ==> a Int Vfrom(X,i) <= b    \
  49.191  \    |] ==> a <= b";
  49.192 -by (rtac (aprem RS subset_univ_eq_Int RS ssubst) 1);
  49.193 +by (stac (aprem RS subset_univ_eq_Int) 1);
  49.194  by (rtac UN_least 1);
  49.195  by (etac iprem 1);
  49.196  qed "univ_Int_Vfrom_subset";
    50.1 --- a/src/ZF/WF.ML	Thu Sep 26 12:50:48 1996 +0200
    50.2 +++ b/src/ZF/WF.ML	Thu Sep 26 15:14:23 1996 +0200
    50.3 @@ -207,7 +207,7 @@
    50.4  
    50.5  val [major] = goalw WF.thy [is_recfun_def]
    50.6      "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)";
    50.7 -by (rtac (major RS ssubst) 1);
    50.8 +by (stac major 1);
    50.9  by (rtac (lamI RS rangeI RS lam_type) 1);
   50.10  by (assume_tac 1);
   50.11  qed "is_recfun_type";
   50.12 @@ -300,7 +300,7 @@
   50.13  goalw WF.thy [wftrec_def]
   50.14      "!!r. [| wf(r);  trans(r) |] ==> \
   50.15  \         wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
   50.16 -by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1);
   50.17 +by (stac (rewrite_rule [is_recfun_def] unfold_the_recfun) 1);
   50.18  by (ALLGOALS (asm_simp_tac
   50.19          (ZF_ss addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut])));
   50.20  qed "wftrec";
   50.21 @@ -310,7 +310,7 @@
   50.22  (*NOT SUITABLE FOR REWRITING since it is recursive!*)
   50.23  val [wfr] = goalw WF.thy [wfrec_def]
   50.24      "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))";
   50.25 -by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1);
   50.26 +by (stac (wfr RS wf_trancl RS wftrec) 1);
   50.27  by (rtac trans_trancl 1);
   50.28  by (rtac (vimage_pair_mono RS restrict_lam_eq RS subst_context) 1);
   50.29  by (etac r_into_trancl 1);
   50.30 @@ -330,7 +330,7 @@
   50.31  \       !!x u. [| x: A;  u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x)   \
   50.32  \    |] ==> wfrec(r,a,H) : B(a)";
   50.33  by (res_inst_tac [("a","a")] wf_induct2 1);
   50.34 -by (rtac (wfrec RS ssubst) 4);
   50.35 +by (stac wfrec 4);
   50.36  by (REPEAT (ares_tac (prems@[lam_type]) 1
   50.37       ORELSE eresolve_tac [spec RS mp, underD] 1));
   50.38  qed "wfrec_type";
    51.1 --- a/src/ZF/add_ind_def.ML	Thu Sep 26 12:50:48 1996 +0200
    51.2 +++ b/src/ZF/add_ind_def.ML	Thu Sep 26 15:14:23 1996 +0200
    51.3 @@ -194,10 +194,10 @@
    51.4      (*Combine split terms using case; yields the case operator for one part*)
    51.5      fun call_case case_list = 
    51.6        let fun call_f (free,[]) = Abs("null", iT, free)
    51.7 -	    | call_f (free,args) =
    51.8 +            | call_f (free,args) =
    51.9                    CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
   51.10 -		              Ind_Syntax.iT 
   51.11 -			      free 
   51.12 +                              Ind_Syntax.iT 
   51.13 +                              free 
   51.14        in  fold_bal (app Su.elim) (map call_f case_list)  end;
   51.15  
   51.16      (** Generating function variables for the case definition
    52.1 --- a/src/ZF/cartprod.ML	Thu Sep 26 12:50:48 1996 +0200
    52.2 +++ b/src/ZF/cartprod.ML	Thu Sep 26 15:14:23 1996 +0200
    52.3 @@ -18,7 +18,7 @@
    52.4    val fsplitE   : thm                   (*elim rule; apparently never used*)
    52.5    end;
    52.6  
    52.7 -signature CARTPROD =		(** Derived syntactic functions for produts **)
    52.8 +signature CARTPROD =            (** Derived syntactic functions for produts **)
    52.9    sig
   52.10    val ap_split : typ -> typ -> term -> term
   52.11    val factors : typ -> typ list
   52.12 @@ -52,8 +52,8 @@
   52.13  
   52.14  (*Make a well-typed instance of "split"*)
   52.15  fun split_const T = Const(Pr.split_name, 
   52.16 -			  [[Ind_Syntax.iT, Ind_Syntax.iT]--->T, 
   52.17 -			   Ind_Syntax.iT] ---> T);
   52.18 +                          [[Ind_Syntax.iT, Ind_Syntax.iT]--->T, 
   52.19 +                           Ind_Syntax.iT] ---> T);
   52.20  
   52.21  (*In ap_split S T u, term u expects separate arguments for the factors of S,
   52.22    with result type T.  The call creates a new term expecting one argument
   52.23 @@ -61,9 +61,9 @@
   52.24  fun ap_split (Type("*", [T1,T2])) T3 u   = 
   52.25         split_const T3 $ 
   52.26         Abs("v", Ind_Syntax.iT, (*Not T1, as it involves pseudo-product types*)
   52.27 -	   ap_split T2 T3
   52.28 -	   ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ 
   52.29 -	    Bound 0))
   52.30 +           ap_split T2 T3
   52.31 +           ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $ 
   52.32 +            Bound 0))
   52.33    | ap_split T T3 u = u;
   52.34  
   52.35  (*Makes a nested tuple from a list, following the product type structure*)
   52.36 @@ -78,11 +78,11 @@
   52.37  (*Uncurries any Var involving pseudo-product type T1 in the rule*)
   52.38  fun split_rule_var (t as Var(v, Type("fun",[T1,T2])), rl) =
   52.39        let val T' = factors T1 ---> T2
   52.40 -	  val newt = ap_split T1 T2 (Var(v,T'))
   52.41 -	  val cterm = Thm.cterm_of (#sign(rep_thm rl))
   52.42 +          val newt = ap_split T1 T2 (Var(v,T'))
   52.43 +          val cterm = Thm.cterm_of (#sign(rep_thm rl))
   52.44        in
   52.45 -	  remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), 
   52.46 -					   cterm newt)]) rl)
   52.47 +          remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)), 
   52.48 +                                           cterm newt)]) rl)
   52.49        end
   52.50    | split_rule_var (t,rl) = rl;
   52.51  
    53.1 --- a/src/ZF/domrange.ML	Thu Sep 26 12:50:48 1996 +0200
    53.2 +++ b/src/ZF/domrange.ML	Thu Sep 26 15:14:23 1996 +0200
    53.3 @@ -79,7 +79,7 @@
    53.4  
    53.5  qed_goalw "range_subset" ZF.thy [range_def] "range(A*B) <= B"
    53.6   (fn _ =>
    53.7 -  [ (rtac (converse_prod RS ssubst) 1),
    53.8 +  [ (stac converse_prod 1),
    53.9      (rtac domain_subset 1) ]);
   53.10  
   53.11  
    54.1 --- a/src/ZF/func.ML	Thu Sep 26 12:50:48 1996 +0200
    54.2 +++ b/src/ZF/func.ML	Thu Sep 26 15:14:23 1996 +0200
    54.3 @@ -184,7 +184,7 @@
    54.4      "(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)";
    54.5  by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1);
    54.6  by (rtac ballI 1);
    54.7 -by (rtac (beta RS ssubst) 1);
    54.8 +by (stac beta 1);
    54.9  by (assume_tac 1);
   54.10  by (etac (major RS theI) 1);
   54.11  qed "lam_theI";
    55.1 --- a/src/ZF/indrule.ML	Thu Sep 26 12:50:48 1996 +0200
    55.2 +++ b/src/ZF/indrule.ML	Thu Sep 26 15:14:23 1996 +0200
    55.3 @@ -83,8 +83,8 @@
    55.4  val min_ss = empty_ss
    55.5        setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
    55.6        setsolver  (fn prems => resolve_tac (triv_rls@prems) 
    55.7 -			      ORELSE' assume_tac
    55.8 -			      ORELSE' etac FalseE);
    55.9 +                              ORELSE' assume_tac
   55.10 +                              ORELSE' etac FalseE);
   55.11  
   55.12  val quant_induct = 
   55.13      prove_goalw_cterm part_rec_defs 
   55.14 @@ -118,13 +118,13 @@
   55.15  fun mk_predpair rec_tm = 
   55.16    let val rec_name = (#1 o dest_Const o head_of) rec_tm
   55.17        val pfree = Free(pred_name ^ "_" ^ rec_name,
   55.18 -		       elem_factors ---> Ind_Syntax.oT)
   55.19 +                       elem_factors ---> Ind_Syntax.oT)
   55.20        val qconcl = 
   55.21          foldr Ind_Syntax.mk_all 
   55.22 -	  (elem_frees, 
   55.23 -	   Ind_Syntax.imp $ 
   55.24 -	   (Ind_Syntax.mem_const $ elem_tuple $ rec_tm)
   55.25 -	         $ (list_comb (pfree, elem_frees)))
   55.26 +          (elem_frees, 
   55.27 +           Ind_Syntax.imp $ 
   55.28 +           (Ind_Syntax.mem_const $ elem_tuple $ rec_tm)
   55.29 +                 $ (list_comb (pfree, elem_frees)))
   55.30    in  (CP.ap_split elem_type Ind_Syntax.oT pfree, 
   55.31         qconcl)  
   55.32    end;
   55.33 @@ -141,15 +141,15 @@
   55.34      Ind_Syntax.mk_tprop
   55.35        (Ind_Syntax.mk_all_imp
   55.36         (big_rec_tm,
   55.37 -	Abs("z", Ind_Syntax.iT, 
   55.38 -	    fold_bal (app Ind_Syntax.conj) 
   55.39 -	    (map mk_rec_imp (Inductive.rec_tms~~preds)))))
   55.40 +        Abs("z", Ind_Syntax.iT, 
   55.41 +            fold_bal (app Ind_Syntax.conj) 
   55.42 +            (map mk_rec_imp (Inductive.rec_tms~~preds)))))
   55.43  and mutual_induct_concl =
   55.44   Ind_Syntax.mk_tprop(fold_bal (app Ind_Syntax.conj) qconcls);
   55.45  
   55.46  val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp],
   55.47 -			resolve_tac [allI, impI, conjI, Part_eqI],
   55.48 -			dresolve_tac [spec, mp, Pr.fsplitD]];
   55.49 +                        resolve_tac [allI, impI, conjI, Part_eqI],
   55.50 +                        dresolve_tac [spec, mp, Pr.fsplitD]];
   55.51  
   55.52  val lemma = (*makes the link between the two induction rules*)
   55.53      prove_goalw_cterm part_rec_defs 
   55.54 @@ -157,7 +157,7 @@
   55.55            (fn prems =>
   55.56             [cut_facts_tac prems 1, 
   55.57              REPEAT (rewrite_goals_tac [Pr.split_eq] THEN
   55.58 -		    lemma_tac 1)]);
   55.59 +                    lemma_tac 1)]);
   55.60  
   55.61  (*Mutual induction follows by freeness of Inl/Inr.*)
   55.62  
   55.63 @@ -190,10 +190,10 @@
   55.64             IF_UNSOLVED (*simp_tac may have finished it off!*)
   55.65               ((*simplify assumptions*)
   55.66                (*some risk of excessive simplification here -- might have
   55.67 -	        to identify the bare minimum set of rewrites*)
   55.68 +                to identify the bare minimum set of rewrites*)
   55.69                full_simp_tac 
   55.70 -	         (mut_ss addsimps (conj_simps @ imp_simps @ quant_simps)) 1
   55.71 -	      THEN
   55.72 +                 (mut_ss addsimps (conj_simps @ imp_simps @ quant_simps)) 1
   55.73 +              THEN
   55.74                (*unpackage and use "prem" in the corresponding place*)
   55.75                REPEAT (rtac impI 1)  THEN
   55.76                rtac (rewrite_rule all_defs prem) 1  THEN
   55.77 @@ -225,7 +225,7 @@
   55.78  val inst = 
   55.79      case elem_frees of [_] => I
   55.80         | _ => instantiate ([], [(cterm_of sign (Var(("x",1), Ind_Syntax.iT)), 
   55.81 -				 cterm_of sign elem_tuple)]);
   55.82 +                                 cterm_of sign elem_tuple)]);
   55.83  
   55.84  (*strip quantifier and the implication*)
   55.85  val induct0 = inst (quant_induct RS spec RSN (2,rev_mp));
   55.86 @@ -236,8 +236,8 @@
   55.87    (*strip quantifier*)
   55.88    val induct = standard 
   55.89                    (CP.split_rule_var
   55.90 -		    (Var((pred_name,2), elem_type --> Ind_Syntax.oT),
   55.91 -		     induct0));
   55.92 +                    (Var((pred_name,2), elem_type --> Ind_Syntax.oT),
   55.93 +                     induct0));
   55.94  
   55.95    (*Just "True" unless there's true mutual recursion.  This saves storage.*)
   55.96    val mutual_induct = 
    56.1 --- a/src/ZF/intr_elim.ML	Thu Sep 26 12:50:48 1996 +0200
    56.2 +++ b/src/ZF/intr_elim.ML	Thu Sep 26 15:14:23 1996 +0200
    56.3 @@ -98,7 +98,7 @@
    56.4  fun intro_tacsf disjIn prems = 
    56.5    [(*insert prems and underlying sets*)
    56.6     cut_facts_tac prems 1,
    56.7 -   DETERM (rtac (unfold RS ssubst) 1),
    56.8 +   DETERM (stac unfold 1),
    56.9     REPEAT (resolve_tac [Part_eqI,CollectI] 1),
   56.10     (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
   56.11     rtac disjIn 2,