eliminated fabs,fapp.
authorslotosch
Wed Aug 12 12:17:20 1998 +0200 (1998-08-12)
changeset 52915706f0ef1d43
parent 5290 b755c7240348
child 5292 92ea5ff34c79
eliminated fabs,fapp.
changed all theorem names and functions into Rep_CFun, Abs_CFun
src/HOLCF/Cfun1.ML
src/HOLCF/Cfun1.thy
src/HOLCF/Cfun2.ML
src/HOLCF/Cfun3.ML
src/HOLCF/Fix.ML
src/HOLCF/IOA/meta_theory/Sequence.ML
src/HOLCF/Lift.ML
src/HOLCF/Lift3.ML
src/HOLCF/Ssum3.ML
src/HOLCF/Up3.ML
src/HOLCF/cont_consts.ML
src/HOLCF/domain/axioms.ML
src/HOLCF/domain/library.ML
src/HOLCF/domain/syntax.ML
src/HOLCF/domain/theorems.ML
src/HOLCF/ex/Hoare.ML
src/HOLCF/ex/Stream.ML
     1.1 --- a/src/HOLCF/Cfun1.ML	Mon Aug 10 17:06:02 1998 +0200
     1.2 +++ b/src/HOLCF/Cfun1.ML	Wed Aug 12 12:17:20 1998 +0200
     1.3 @@ -9,22 +9,22 @@
     1.4  open Cfun1;
     1.5  
     1.6  (* ------------------------------------------------------------------------ *)
     1.7 -(* derive old type definition rules for fabs & fapp                         *)
     1.8 -(* fapp and fabs should be replaced by Rep_Cfun anf Abs_Cfun in future      *)
     1.9 +(* derive old type definition rules for Abs_CFun & Rep_CFun                         *)
    1.10 +(* Rep_CFun and Abs_CFun should be replaced by Rep_Cfun anf Abs_Cfun in future      *)
    1.11  (* ------------------------------------------------------------------------ *)
    1.12 -qed_goalw "Rep_Cfun" thy [fapp_def] "fapp fo : CFun"
    1.13 +qed_goal "Rep_Cfun" thy "Rep_CFun fo : CFun"
    1.14  (fn prems =>
    1.15          [
    1.16          (rtac Rep_CFun 1)
    1.17          ]);
    1.18  
    1.19 -qed_goalw "Rep_Cfun_inverse" thy [fapp_def,fabs_def] "fabs (fapp fo) = fo"
    1.20 +qed_goal "Rep_Cfun_inverse" thy "Abs_CFun (Rep_CFun fo) = fo"
    1.21  (fn prems =>
    1.22          [
    1.23          (rtac Rep_CFun_inverse 1)
    1.24          ]);
    1.25  
    1.26 -qed_goalw "Abs_Cfun_inverse" thy [fapp_def,fabs_def] "f:CFun==>fapp(fabs f)=f"
    1.27 +qed_goal "Abs_Cfun_inverse" thy "f:CFun==>Rep_CFun(Abs_CFun f)=f"
    1.28  (fn prems =>
    1.29          [
    1.30  	(cut_facts_tac prems 1),
    1.31 @@ -97,7 +97,7 @@
    1.32  (* additional lemma about the isomorphism between -> and Cfun               *)
    1.33  (* ------------------------------------------------------------------------ *)
    1.34  
    1.35 -qed_goal "Abs_Cfun_inverse2" thy "cont f ==> fapp (fabs f) = f"
    1.36 +qed_goal "Abs_Cfun_inverse2" thy "cont f ==> Rep_CFun (Abs_CFun f) = f"
    1.37  (fn prems =>
    1.38          [
    1.39          (cut_facts_tac prems 1),
    1.40 @@ -110,7 +110,7 @@
    1.41  (* simplification of application                                            *)
    1.42  (* ------------------------------------------------------------------------ *)
    1.43  
    1.44 -qed_goal "Cfunapp2" thy "cont f ==> (fabs f)`x = f x"
    1.45 +qed_goal "Cfunapp2" thy "cont f ==> (Abs_CFun f)`x = f x"
    1.46  (fn prems =>
    1.47          [
    1.48          (cut_facts_tac prems 1),
     2.1 --- a/src/HOLCF/Cfun1.thy	Mon Aug 10 17:06:02 1998 +0200
     2.2 +++ b/src/HOLCF/Cfun1.thy	Wed Aug 12 12:17:20 1998 +0200
     2.3 @@ -16,12 +16,10 @@
     2.4  (* to make << defineable *)
     2.5  instance "->"  :: (cpo,cpo)sq_ord
     2.6  
     2.7 -consts  
     2.8 -        fapp      :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999)
     2.9 -					        (* usually Rep_Cfun *)
    2.10 +syntax
    2.11 +	Rep_CFun  :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999)
    2.12                                                  (* application      *)
    2.13 -        fabs      :: "('a => 'b)=>('a -> 'b)"     (binder "LAM " 10)
    2.14 -                                                (* usually Abs_Cfun *)
    2.15 +        Abs_CFun  :: "('a => 'b)=>('a -> 'b)"     (binder "LAM " 10)
    2.16                                                  (* abstraction      *)
    2.17          less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
    2.18  
    2.19 @@ -30,9 +28,6 @@
    2.20    "LAM "	:: "[idts, 'a => 'b] => ('a -> 'b)"
    2.21  					("(3\\<Lambda>_./ _)" [0, 10] 10)
    2.22  defs 
    2.23 -  fabs_def	"fabs==Abs_CFun"
    2.24 -  fapp_def	"fapp==Rep_CFun"
    2.25 -
    2.26 -  less_cfun_def "(op <<) == (% fo1 fo2. fapp fo1 << fapp fo2 )"
    2.27 +  less_cfun_def "(op <<) == (% fo1 fo2. Rep_CFun fo1 << Rep_CFun fo2 )"
    2.28  
    2.29  end
     3.1 --- a/src/HOLCF/Cfun2.ML	Mon Aug 10 17:06:02 1998 +0200
     3.2 +++ b/src/HOLCF/Cfun2.ML	Wed Aug 12 12:17:20 1998 +0200
     3.3 @@ -9,7 +9,7 @@
     3.4  open Cfun2;
     3.5  
     3.6  (* for compatibility with old HOLCF-Version *)
     3.7 -qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2. fapp f1 << fapp f2)"
     3.8 +qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2. Rep_CFun f1 << Rep_CFun f2)"
     3.9   (fn prems => 
    3.10          [
    3.11  	(fold_goals_tac [less_cfun_def]),
    3.12 @@ -20,7 +20,7 @@
    3.13  (* access to less_cfun in class po                                          *)
    3.14  (* ------------------------------------------------------------------------ *)
    3.15  
    3.16 -qed_goal "less_cfun" thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
    3.17 +qed_goal "less_cfun" thy "( f1 << f2 ) = (Rep_CFun(f1) << Rep_CFun(f2))"
    3.18  (fn prems =>
    3.19          [
    3.20          (simp_tac (simpset() addsimps [inst_cfun_po]) 1)
    3.21 @@ -30,7 +30,7 @@
    3.22  (* Type 'a ->'b  is pointed                                                 *)
    3.23  (* ------------------------------------------------------------------------ *)
    3.24  
    3.25 -qed_goal "minimal_cfun" thy "fabs(% x. UU) << f"
    3.26 +qed_goal "minimal_cfun" thy "Abs_CFun(% x. UU) << f"
    3.27  (fn prems =>
    3.28          [
    3.29          (stac less_cfun 1),
    3.30 @@ -44,17 +44,17 @@
    3.31  qed_goal "least_cfun" thy "? x::'a->'b::pcpo.!y. x<<y"
    3.32  (fn prems =>
    3.33          [
    3.34 -        (res_inst_tac [("x","fabs(% x. UU)")] exI 1),
    3.35 +        (res_inst_tac [("x","Abs_CFun(% x. UU)")] exI 1),
    3.36          (rtac (minimal_cfun RS allI) 1)
    3.37          ]);
    3.38  
    3.39  (* ------------------------------------------------------------------------ *)
    3.40 -(* fapp yields continuous functions in 'a => 'b                             *)
    3.41 -(* this is continuity of fapp in its 'second' argument                      *)
    3.42 -(* cont_fapp2 ==> monofun_fapp2 & contlub_fapp2                            *)
    3.43 +(* Rep_CFun yields continuous functions in 'a => 'b                             *)
    3.44 +(* this is continuity of Rep_CFun in its 'second' argument                      *)
    3.45 +(* cont_Rep_CFun2 ==> monofun_Rep_CFun2 & contlub_Rep_CFun2                            *)
    3.46  (* ------------------------------------------------------------------------ *)
    3.47  
    3.48 -qed_goal "cont_fapp2" thy "cont(fapp(fo))"
    3.49 +qed_goal "cont_Rep_CFun2" thy "cont(Rep_CFun(fo))"
    3.50  (fn prems =>
    3.51          [
    3.52          (res_inst_tac [("P","cont")] CollectD 1),
    3.53 @@ -62,30 +62,30 @@
    3.54          (rtac Rep_Cfun 1)
    3.55          ]);
    3.56  
    3.57 -bind_thm ("monofun_fapp2", cont_fapp2 RS cont2mono);
    3.58 -(* monofun(fapp(?fo1)) *)
    3.59 +bind_thm ("monofun_Rep_CFun2", cont_Rep_CFun2 RS cont2mono);
    3.60 +(* monofun(Rep_CFun(?fo1)) *)
    3.61  
    3.62  
    3.63 -bind_thm ("contlub_fapp2", cont_fapp2 RS cont2contlub);
    3.64 -(* contlub(fapp(?fo1)) *)
    3.65 +bind_thm ("contlub_Rep_CFun2", cont_Rep_CFun2 RS cont2contlub);
    3.66 +(* contlub(Rep_CFun(?fo1)) *)
    3.67  
    3.68  (* ------------------------------------------------------------------------ *)
    3.69 -(* expanded thms cont_fapp2, contlub_fapp2                                 *)
    3.70 +(* expanded thms cont_Rep_CFun2, contlub_Rep_CFun2                                 *)
    3.71  (* looks nice with mixfix syntac                                            *)
    3.72  (* ------------------------------------------------------------------------ *)
    3.73  
    3.74 -bind_thm ("cont_cfun_arg", (cont_fapp2 RS contE RS spec RS mp));
    3.75 +bind_thm ("cont_cfun_arg", (cont_Rep_CFun2 RS contE RS spec RS mp));
    3.76  (* chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1))    *)
    3.77   
    3.78 -bind_thm ("contlub_cfun_arg", (contlub_fapp2 RS contlubE RS spec RS mp));
    3.79 +bind_thm ("contlub_cfun_arg", (contlub_Rep_CFun2 RS contlubE RS spec RS mp));
    3.80  (* chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
    3.81  
    3.82  
    3.83  (* ------------------------------------------------------------------------ *)
    3.84 -(* fapp is monotone in its 'first' argument                                 *)
    3.85 +(* Rep_CFun is monotone in its 'first' argument                                 *)
    3.86  (* ------------------------------------------------------------------------ *)
    3.87  
    3.88 -qed_goalw "monofun_fapp1" thy [monofun] "monofun(fapp)"
    3.89 +qed_goalw "monofun_Rep_CFun1" thy [monofun] "monofun(Rep_CFun)"
    3.90  (fn prems =>
    3.91          [
    3.92          (strip_tac 1),
    3.93 @@ -94,7 +94,7 @@
    3.94  
    3.95  
    3.96  (* ------------------------------------------------------------------------ *)
    3.97 -(* monotonicity of application fapp in mixfix syntax [_]_                   *)
    3.98 +(* monotonicity of application Rep_CFun in mixfix syntax [_]_                   *)
    3.99  (* ------------------------------------------------------------------------ *)
   3.100  
   3.101  qed_goal "monofun_cfun_fun" thy  "f1 << f2 ==> f1`x << f2`x"
   3.102 @@ -103,15 +103,15 @@
   3.103          (cut_facts_tac prems 1),
   3.104          (res_inst_tac [("x","x")] spec 1),
   3.105          (rtac (less_fun RS subst) 1),
   3.106 -        (etac (monofun_fapp1 RS monofunE RS spec RS spec RS mp) 1)
   3.107 +        (etac (monofun_Rep_CFun1 RS monofunE RS spec RS spec RS mp) 1)
   3.108          ]);
   3.109  
   3.110  
   3.111 -bind_thm ("monofun_cfun_arg", monofun_fapp2 RS monofunE RS spec RS spec RS mp);
   3.112 +bind_thm ("monofun_cfun_arg", monofun_Rep_CFun2 RS monofunE RS spec RS spec RS mp);
   3.113  (* ?x2 << ?x1 ==> ?fo5`?x2 << ?fo5`?x1                                      *)
   3.114  
   3.115  (* ------------------------------------------------------------------------ *)
   3.116 -(* monotonicity of fapp in both arguments in mixfix syntax [_]_             *)
   3.117 +(* monotonicity of Rep_CFun in both arguments in mixfix syntax [_]_             *)
   3.118  (* ------------------------------------------------------------------------ *)
   3.119  
   3.120  qed_goal "monofun_cfun" thy
   3.121 @@ -137,16 +137,16 @@
   3.122  (* use MF2 lemmas from Cont.ML                                              *)
   3.123  (* ------------------------------------------------------------------------ *)
   3.124  
   3.125 -qed_goal "ch2ch_fappR" thy 
   3.126 +qed_goal "ch2ch_Rep_CFunR" thy 
   3.127   "chain(Y) ==> chain(%i. f`(Y i))"
   3.128  (fn prems =>
   3.129          [
   3.130          (cut_facts_tac prems 1),
   3.131 -        (etac (monofun_fapp2 RS ch2ch_MF2R) 1)
   3.132 +        (etac (monofun_Rep_CFun2 RS ch2ch_MF2R) 1)
   3.133          ]);
   3.134  
   3.135  
   3.136 -bind_thm ("ch2ch_fappL", monofun_fapp1 RS ch2ch_MF2L);
   3.137 +bind_thm ("ch2ch_Rep_CFunL", monofun_Rep_CFun1 RS ch2ch_MF2L);
   3.138  (* chain(?F) ==> chain (%i. ?F i`?x)                                  *)
   3.139  
   3.140  
   3.141 @@ -161,8 +161,8 @@
   3.142          [
   3.143          (cut_facts_tac prems 1),
   3.144          (rtac lub_MF2_mono 1),
   3.145 -        (rtac monofun_fapp1 1),
   3.146 -        (rtac (monofun_fapp2 RS allI) 1),
   3.147 +        (rtac monofun_Rep_CFun1 1),
   3.148 +        (rtac (monofun_Rep_CFun2 RS allI) 1),
   3.149          (atac 1)
   3.150          ]);
   3.151  
   3.152 @@ -179,8 +179,8 @@
   3.153          [
   3.154          (cut_facts_tac prems 1),
   3.155          (rtac ex_lubMF2 1),
   3.156 -        (rtac monofun_fapp1 1),
   3.157 -        (rtac (monofun_fapp2 RS allI) 1),
   3.158 +        (rtac monofun_Rep_CFun1 1),
   3.159 +        (rtac (monofun_Rep_CFun2 RS allI) 1),
   3.160          (atac 1),
   3.161          (atac 1)
   3.162          ]);
   3.163 @@ -221,14 +221,14 @@
   3.164          (stac Abs_Cfun_inverse2 1),
   3.165          (etac cont_lubcfun 1),
   3.166          (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
   3.167 -        (etac (monofun_fapp1 RS ch2ch_monofun) 1),
   3.168 +        (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
   3.169          (strip_tac 1),
   3.170          (stac less_cfun 1),
   3.171          (stac Abs_Cfun_inverse2 1),
   3.172          (etac cont_lubcfun 1),
   3.173          (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
   3.174 -        (etac (monofun_fapp1 RS ch2ch_monofun) 1),
   3.175 -        (etac (monofun_fapp1 RS ub2ub_monofun) 1)
   3.176 +        (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
   3.177 +        (etac (monofun_Rep_CFun1 RS ub2ub_monofun) 1)
   3.178          ]);
   3.179  
   3.180  bind_thm ("thelub_cfun", lub_cfun RS thelubI);
   3.181 @@ -255,17 +255,17 @@
   3.182          [
   3.183          (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   3.184          (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
   3.185 -        (res_inst_tac [("f","fabs")] arg_cong 1),
   3.186 +        (res_inst_tac [("f","Abs_CFun")] arg_cong 1),
   3.187          (rtac ext 1),
   3.188          (resolve_tac prems 1)
   3.189          ]);
   3.190  
   3.191  (* ------------------------------------------------------------------------ *)
   3.192 -(* Monotonicity of fabs                                                     *)
   3.193 +(* Monotonicity of Abs_CFun                                                     *)
   3.194  (* ------------------------------------------------------------------------ *)
   3.195  
   3.196 -qed_goal "semi_monofun_fabs" thy 
   3.197 -        "[|cont(f);cont(g);f<<g|]==>fabs(f)<<fabs(g)"
   3.198 +qed_goal "semi_monofun_Abs_CFun" thy 
   3.199 +        "[|cont(f);cont(g);f<<g|]==>Abs_CFun(f)<<Abs_CFun(g)"
   3.200   (fn prems =>
   3.201          [
   3.202          (rtac (less_cfun RS iffD2) 1),
   3.203 @@ -285,9 +285,9 @@
   3.204          [
   3.205          (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
   3.206          (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
   3.207 -        (rtac semi_monofun_fabs 1),
   3.208 -        (rtac cont_fapp2 1),
   3.209 -        (rtac cont_fapp2 1),
   3.210 +        (rtac semi_monofun_Abs_CFun 1),
   3.211 +        (rtac cont_Rep_CFun2 1),
   3.212 +        (rtac cont_Rep_CFun2 1),
   3.213          (rtac (less_fun RS iffD2) 1),
   3.214          (rtac allI 1),
   3.215          (resolve_tac prems 1)
     4.1 --- a/src/HOLCF/Cfun3.ML	Mon Aug 10 17:06:02 1998 +0200
     4.2 +++ b/src/HOLCF/Cfun3.ML	Wed Aug 12 12:17:20 1998 +0200
     4.3 @@ -7,17 +7,17 @@
     4.4  open Cfun3;
     4.5  
     4.6  (* for compatibility with old HOLCF-Version *)
     4.7 -qed_goal "inst_cfun_pcpo" thy "UU = fabs(%x. UU)"
     4.8 +qed_goal "inst_cfun_pcpo" thy "UU = Abs_CFun(%x. UU)"
     4.9   (fn prems => 
    4.10          [
    4.11          (simp_tac (HOL_ss addsimps [UU_def,UU_cfun_def]) 1)
    4.12          ]);
    4.13  
    4.14  (* ------------------------------------------------------------------------ *)
    4.15 -(* the contlub property for fapp its 'first' argument                       *)
    4.16 +(* the contlub property for Rep_CFun its 'first' argument                       *)
    4.17  (* ------------------------------------------------------------------------ *)
    4.18  
    4.19 -qed_goal "contlub_fapp1" thy "contlub(fapp)"
    4.20 +qed_goal "contlub_Rep_CFun1" thy "contlub(Rep_CFun)"
    4.21  (fn prems =>
    4.22          [
    4.23          (rtac contlubI 1),
    4.24 @@ -29,26 +29,26 @@
    4.25          (stac Cfunapp2 1),
    4.26          (etac cont_lubcfun 1),
    4.27          (stac thelub_fun 1),
    4.28 -        (etac (monofun_fapp1 RS ch2ch_monofun) 1),
    4.29 +        (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
    4.30          (rtac refl 1)
    4.31          ]);
    4.32  
    4.33  
    4.34  (* ------------------------------------------------------------------------ *)
    4.35 -(* the cont property for fapp in its first argument                        *)
    4.36 +(* the cont property for Rep_CFun in its first argument                        *)
    4.37  (* ------------------------------------------------------------------------ *)
    4.38  
    4.39 -qed_goal "cont_fapp1" thy "cont(fapp)"
    4.40 +qed_goal "cont_Rep_CFun1" thy "cont(Rep_CFun)"
    4.41  (fn prems =>
    4.42          [
    4.43          (rtac monocontlub2cont 1),
    4.44 -        (rtac monofun_fapp1 1),
    4.45 -        (rtac contlub_fapp1 1)
    4.46 +        (rtac monofun_Rep_CFun1 1),
    4.47 +        (rtac contlub_Rep_CFun1 1)
    4.48          ]);
    4.49  
    4.50  
    4.51  (* ------------------------------------------------------------------------ *)
    4.52 -(* contlub, cont properties of fapp in its first argument in mixfix _[_]   *)
    4.53 +(* contlub, cont properties of Rep_CFun in its first argument in mixfix _[_]   *)
    4.54  (* ------------------------------------------------------------------------ *)
    4.55  
    4.56  qed_goal "contlub_cfun_fun" thy 
    4.57 @@ -58,9 +58,9 @@
    4.58          [
    4.59          (cut_facts_tac prems 1),
    4.60          (rtac trans 1),
    4.61 -        (etac (contlub_fapp1 RS contlubE RS spec RS mp RS fun_cong) 1),
    4.62 +        (etac (contlub_Rep_CFun1 RS contlubE RS spec RS mp RS fun_cong) 1),
    4.63          (stac thelub_fun 1),
    4.64 -        (etac (monofun_fapp1 RS ch2ch_monofun) 1),
    4.65 +        (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
    4.66          (rtac refl 1)
    4.67          ]);
    4.68  
    4.69 @@ -72,13 +72,13 @@
    4.70          [
    4.71          (cut_facts_tac prems 1),
    4.72          (rtac thelubE 1),
    4.73 -        (etac ch2ch_fappL 1),
    4.74 +        (etac ch2ch_Rep_CFunL 1),
    4.75          (etac (contlub_cfun_fun RS sym) 1)
    4.76          ]);
    4.77  
    4.78  
    4.79  (* ------------------------------------------------------------------------ *)
    4.80 -(* contlub, cont  properties of fapp in both argument in mixfix _[_]       *)
    4.81 +(* contlub, cont  properties of Rep_CFun in both argument in mixfix _[_]       *)
    4.82  (* ------------------------------------------------------------------------ *)
    4.83  
    4.84  qed_goal "contlub_cfun" thy 
    4.85 @@ -88,9 +88,9 @@
    4.86          [
    4.87          (cut_facts_tac prems 1),
    4.88          (rtac contlub_CF2 1),
    4.89 -        (rtac cont_fapp1 1),
    4.90 +        (rtac cont_Rep_CFun1 1),
    4.91          (rtac allI 1),
    4.92 -        (rtac cont_fapp2 1),
    4.93 +        (rtac cont_Rep_CFun2 1),
    4.94          (atac 1),
    4.95          (atac 1)
    4.96          ]);
    4.97 @@ -102,9 +102,9 @@
    4.98          [
    4.99          (cut_facts_tac prems 1),
   4.100          (rtac thelubE 1),
   4.101 -        (rtac (monofun_fapp1 RS ch2ch_MF2LR) 1),
   4.102 +        (rtac (monofun_Rep_CFun1 RS ch2ch_MF2LR) 1),
   4.103          (rtac allI 1),
   4.104 -        (rtac monofun_fapp2 1),
   4.105 +        (rtac monofun_Rep_CFun2 1),
   4.106          (atac 1),
   4.107          (atac 1),
   4.108          (etac (contlub_cfun RS sym) 1),
   4.109 @@ -113,10 +113,10 @@
   4.110  
   4.111  
   4.112  (* ------------------------------------------------------------------------ *)
   4.113 -(* cont2cont lemma for fapp                                               *)
   4.114 +(* cont2cont lemma for Rep_CFun                                               *)
   4.115  (* ------------------------------------------------------------------------ *)
   4.116  
   4.117 -qed_goal "cont2cont_fapp" thy 
   4.118 +qed_goal "cont2cont_Rep_CFun" thy 
   4.119          "[|cont(%x. ft x);cont(%x. tt x)|] ==> cont(%x. (ft x)`(tt x))"
   4.120   (fn prems =>
   4.121          [
   4.122 @@ -124,9 +124,9 @@
   4.123          (rtac cont2cont_app2 1),
   4.124          (rtac cont2cont_app2 1),
   4.125          (rtac cont_const 1),
   4.126 -        (rtac cont_fapp1 1),
   4.127 +        (rtac cont_Rep_CFun1 1),
   4.128          (atac 1),
   4.129 -        (rtac cont_fapp2 1),
   4.130 +        (rtac cont_Rep_CFun2 1),
   4.131          (atac 1)
   4.132          ]);
   4.133  
   4.134 @@ -169,7 +169,7 @@
   4.135          (rtac (p1 RS cont2mono_LAM RS ch2ch_monofun) 1),
   4.136          (rtac (p2 RS cont2mono) 1),
   4.137          (atac 1),
   4.138 -        (res_inst_tac [("f","fabs")] arg_cong 1),
   4.139 +        (res_inst_tac [("f","Abs_CFun")] arg_cong 1),
   4.140          (rtac ext 1),
   4.141          (stac (p1 RS beta_cfun RS ext) 1),
   4.142          (etac (p2 RS cont2contlub RS contlubE RS spec RS mp) 1)
   4.143 @@ -179,8 +179,8 @@
   4.144  (* cont2cont tactic                                                       *)
   4.145  (* ------------------------------------------------------------------------ *)
   4.146  
   4.147 -val cont_lemmas1 = [cont_const, cont_id, cont_fapp2,
   4.148 -                    cont2cont_fapp,cont2cont_LAM];
   4.149 +val cont_lemmas1 = [cont_const, cont_id, cont_Rep_CFun2,
   4.150 +                    cont2cont_Rep_CFun,cont2cont_LAM];
   4.151  
   4.152  Addsimps cont_lemmas1;
   4.153  
   4.154 @@ -193,7 +193,7 @@
   4.155  (* function application _[_]  is strict in its first arguments              *)
   4.156  (* ------------------------------------------------------------------------ *)
   4.157  
   4.158 -qed_goal "strict_fapp1" thy "(UU::'a::cpo->'b)`x = (UU::'b)"
   4.159 +qed_goal "strict_Rep_CFun1" thy "(UU::'a::cpo->'b)`x = (UU::'b)"
   4.160   (fn prems =>
   4.161          [
   4.162          (stac inst_cfun_pcpo 1),
   4.163 @@ -322,7 +322,7 @@
   4.164          (rtac (Istrictify2 RS sym) 1),
   4.165          (fast_tac HOL_cs 1),
   4.166          (rtac ch2ch_monofun 1),
   4.167 -        (rtac monofun_fapp2 1),
   4.168 +        (rtac monofun_Rep_CFun2 1),
   4.169          (atac 1),
   4.170          (rtac ch2ch_monofun 1),
   4.171          (rtac monofun_Istrictify2 1),
   4.172 @@ -362,7 +362,7 @@
   4.173  (* Instantiate the simplifier                                               *)
   4.174  (* ------------------------------------------------------------------------ *)
   4.175  
   4.176 -Addsimps [minimal,refl_less,beta_cfun,strict_fapp1,strictify1, strictify2];
   4.177 +Addsimps [minimal,refl_less,beta_cfun,strict_Rep_CFun1,strictify1, strictify2];
   4.178  
   4.179  
   4.180  (* ------------------------------------------------------------------------ *)
   4.181 @@ -376,7 +376,7 @@
   4.182  (* some lemmata for functions with flat/chfin domain/range types	    *)
   4.183  (* ------------------------------------------------------------------------ *)
   4.184  
   4.185 -qed_goal "chfin_fappR" thy 
   4.186 +qed_goal "chfin_Rep_CFunR" thy 
   4.187      "chain (Y::nat => 'a::cpo->'b::chfin)==> !s. ? n. lub(range(Y))`s = Y n`s" 
   4.188  (fn prems => 
   4.189  	[
   4.190 @@ -384,7 +384,7 @@
   4.191  	rtac allI 1,
   4.192  	stac contlub_cfun_fun 1,
   4.193  	 atac 1,
   4.194 -	fast_tac (HOL_cs addSIs [thelubI,chfin,lub_finch2,chfin2finch,ch2ch_fappL])1
   4.195 +	fast_tac (HOL_cs addSIs [thelubI,chfin,lub_finch2,chfin2finch,ch2ch_Rep_CFunL])1
   4.196  	]);
   4.197  
   4.198  (* ------------------------------------------------------------------------ *)
   4.199 @@ -451,7 +451,7 @@
   4.200          (rtac exE 1),
   4.201          (res_inst_tac [("P","chain(%i. g`(Y i))")] mp 1),
   4.202          (etac spec 1),
   4.203 -        (etac ch2ch_fappR 1),
   4.204 +        (etac ch2ch_Rep_CFunR 1),
   4.205          (rtac exI 1),
   4.206          (strip_tac 1),
   4.207          (res_inst_tac [("s","f`(g`(Y x))"),("t","Y(x)")] subst 1),
     5.1 --- a/src/HOLCF/Fix.ML	Mon Aug 10 17:06:02 1998 +0200
     5.2 +++ b/src/HOLCF/Fix.ML	Wed Aug 12 12:17:20 1998 +0200
     5.3 @@ -65,13 +65,13 @@
     5.4          (rtac antisym_less 1),
     5.5          (rtac lub_mono 1),
     5.6          (rtac chain_iterate 1),
     5.7 -        (rtac ch2ch_fappR 1),
     5.8 +        (rtac ch2ch_Rep_CFunR 1),
     5.9          (rtac chain_iterate 1),
    5.10          (rtac allI 1),
    5.11          (rtac (iterate_Suc RS subst) 1),
    5.12          (rtac (chain_iterate RS chainE RS spec) 1),
    5.13          (rtac is_lub_thelub 1),
    5.14 -        (rtac ch2ch_fappR 1),
    5.15 +        (rtac ch2ch_Rep_CFunR 1),
    5.16          (rtac chain_iterate 1),
    5.17          (rtac ub_rangeI 1),
    5.18          (rtac allI 1),
    5.19 @@ -120,7 +120,7 @@
    5.20  (* ------------------------------------------------------------------------ *)
    5.21  (* the following lemma uses contlub_cfun which itself is based on a         *)
    5.22  (* diagonalisation lemma for continuous functions with two arguments.       *)
    5.23 -(* In this special case it is the application function fapp                 *)
    5.24 +(* In this special case it is the application function Rep_CFun                 *)
    5.25  (* ------------------------------------------------------------------------ *)
    5.26  
    5.27  qed_goalw "contlub_iterate" thy  [contlub] "contlub(iterate(i))"
    5.28 @@ -138,9 +138,9 @@
    5.29          (rtac (less_fun RS iffD2) 1),
    5.30          (rtac allI 1),
    5.31          (rtac (chainE RS spec) 1),
    5.32 -        (rtac (monofun_fapp1 RS ch2ch_MF2LR) 1),
    5.33 +        (rtac (monofun_Rep_CFun1 RS ch2ch_MF2LR) 1),
    5.34          (rtac allI 1),
    5.35 -        (rtac monofun_fapp2 1),
    5.36 +        (rtac monofun_Rep_CFun2 1),
    5.37          (atac 1),
    5.38          (rtac ch2ch_fun 1),
    5.39          (rtac (monofun_iterate RS ch2ch_monofun) 1),
    5.40 @@ -547,7 +547,7 @@
    5.41  qed_goalw "adm_chfindom" thy [adm_def] "adm (%(u::'a::cpo->'b::chfin). P(u`s))"
    5.42      (fn _ => [
    5.43  	strip_tac 1,
    5.44 -	dtac chfin_fappR 1,
    5.45 +	dtac chfin_Rep_CFunR 1,
    5.46  	eres_inst_tac [("x","s")] allE 1,
    5.47  	fast_tac (HOL_cs addss (simpset() addsimps [chfin])) 1]);
    5.48  
     6.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Mon Aug 10 17:06:02 1998 +0200
     6.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Wed Aug 12 12:17:20 1998 +0200
     6.3 @@ -924,8 +924,8 @@
     6.4  by (stac contlub_cfun_fun 1);
     6.5  by (rtac chain_iterate 1);
     6.6  by (rtac lub_mono 1);
     6.7 -by (rtac (chain_iterate RS ch2ch_fappL) 1);
     6.8 -by (rtac (chain_iterate RS ch2ch_fappL) 1);
     6.9 +by (rtac (chain_iterate RS ch2ch_Rep_CFunL) 1);
    6.10 +by (rtac (chain_iterate RS ch2ch_Rep_CFunL) 1);
    6.11  by (rtac allI 1);
    6.12  by (resolve_tac prems 1);
    6.13  qed"take_lemma_less1";
     7.1 --- a/src/HOLCF/Lift.ML	Mon Aug 10 17:06:02 1998 +0200
     7.2 +++ b/src/HOLCF/Lift.ML	Wed Aug 12 12:17:20 1998 +0200
     7.3 @@ -58,7 +58,7 @@
     7.4  
     7.5  val cont_lemmas_ext = [cont_flift1_arg,cont_flift2_arg,
     7.6                         cont_flift1_arg_and_not_arg,cont2cont_CF1L_rev2, 
     7.7 -                       cont_fapp_app,cont_fapp_app_app,cont_if];
     7.8 +                       cont_Rep_CFun_app,cont_Rep_CFun_app_app,cont_if];
     7.9  
    7.10  val cont_lemmas2 =  cont_lemmas1 @ cont_lemmas_ext;
    7.11                   
     8.1 --- a/src/HOLCF/Lift3.ML	Mon Aug 10 17:06:02 1998 +0200
     8.2 +++ b/src/HOLCF/Lift3.ML	Wed Aug 12 12:17:20 1998 +0200
     8.3 @@ -143,13 +143,13 @@
     8.4  by (rtac cont2cont_CF1L 1);
     8.5  by (REPEAT (resolve_tac cont_lemmas1 1));
     8.6  by Auto_tac;
     8.7 -qed"cont_fapp_app";
     8.8 +qed"cont_Rep_CFun_app";
     8.9  
    8.10  Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
    8.11  by (rtac cont2cont_CF1L 1);
    8.12 -by (etac cont_fapp_app 1);
    8.13 +by (etac cont_Rep_CFun_app 1);
    8.14  by (assume_tac 1);
    8.15 -qed"cont_fapp_app_app";
    8.16 +qed"cont_Rep_CFun_app_app";
    8.17  
    8.18  
    8.19  (* continuity of if then else *)
     9.1 --- a/src/HOLCF/Ssum3.ML	Mon Aug 10 17:06:02 1998 +0200
     9.2 +++ b/src/HOLCF/Ssum3.ML	Wed Aug 12 12:17:20 1998 +0200
     9.3 @@ -262,7 +262,7 @@
     9.4          (atac 1),
     9.5          (fast_tac HOL_cs 1),
     9.6          (simp_tac (simpset_of Cfun3.thy) 1),
     9.7 -        (rtac (monofun_fapp2 RS ch2ch_monofun) 1),
     9.8 +        (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 1),
     9.9          (etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
    9.10          (etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
    9.11          ]);
    9.12 @@ -326,7 +326,7 @@
    9.13          (atac 1),
    9.14          (fast_tac HOL_cs 1),
    9.15          (simp_tac (simpset_of Cfun3.thy) 1),
    9.16 -        (rtac (monofun_fapp2 RS ch2ch_monofun) 1),
    9.17 +        (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 1),
    9.18          (etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
    9.19          (etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
    9.20          ]);
    10.1 --- a/src/HOLCF/Up3.ML	Mon Aug 10 17:06:02 1998 +0200
    10.2 +++ b/src/HOLCF/Up3.ML	Wed Aug 12 12:17:20 1998 +0200
    10.3 @@ -110,7 +110,7 @@
    10.4          (stac contlub_cfun_arg 1),
    10.5          (etac (monofun_Ifup2 RS ch2ch_monofun) 1),
    10.6          (rtac lub_equal2 1),
    10.7 -        (rtac (monofun_fapp2 RS ch2ch_monofun) 2),
    10.8 +        (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 2),
    10.9          (etac (monofun_Ifup2 RS ch2ch_monofun) 2),
   10.10          (etac (monofun_Ifup2 RS ch2ch_monofun) 2),
   10.11          (rtac (chain_mono2 RS exE) 1),
    11.1 --- a/src/HOLCF/cont_consts.ML	Mon Aug 10 17:06:02 1998 +0200
    11.2 +++ b/src/HOLCF/cont_consts.ML	Wed Aug 12 12:17:20 1998 +0200
    11.3 @@ -35,7 +35,7 @@
    11.4    val vnames = argnames (ord "A") n;
    11.5    val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1);
    11.6    in [Syntax.ParsePrintRule (Ast.mk_appl (Constant name2) (map Variable vnames),
    11.7 -			  foldl (fn (t,arg) => (Ast.mk_appl (Constant "fapp") 
    11.8 +			  foldl (fn (t,arg) => (Ast.mk_appl (Constant "Rep_CFun") 
    11.9  						[t,Variable arg]))
   11.10  			  (Constant name1,vnames))]
   11.11       @(case mx of InfixlName _ => [extra_parse_rule] 
    12.1 --- a/src/HOLCF/domain/axioms.ML	Mon Aug 10 17:06:02 1998 +0200
    12.2 +++ b/src/HOLCF/domain/axioms.ML	Wed Aug 12 12:17:20 1998 +0200
    12.3 @@ -57,14 +57,14 @@
    12.4  
    12.5    val dis_defs = let
    12.6  	fun ddef (con,_) = (dis_name con ^"_def",%%(dis_name con) == 
    12.7 -		 mk_cfapp(%%(dname^"_when"),map 
    12.8 +		 mk_cRep_CFun(%%(dname^"_when"),map 
    12.9  			(fn (con',args) => (foldr /\#
   12.10  			   (args,if con'=con then %%"TT" else %%"FF"))) cons))
   12.11  	in map ddef cons end;
   12.12  
   12.13    val sel_defs = let
   12.14  	fun sdef con n arg = (sel_of arg^"_def",%%(sel_of arg) == 
   12.15 -		 mk_cfapp(%%(dname^"_when"),map 
   12.16 +		 mk_cRep_CFun(%%(dname^"_when"),map 
   12.17  			(fn (con',args) => if con'<>con then %%"UU" else
   12.18  			 foldr /\# (args,Bound (length args - n))) cons));
   12.19  	in flat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end;
   12.20 @@ -116,8 +116,8 @@
   12.21  	fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ 
   12.22  			   Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
   12.23  	val capps = foldr mk_conj (mapn rel_app 1 rec_args, mk_conj(
   12.24 -	   Bound(allargs_cnt+1)===mk_cfapp(%%con,map (bound_arg allvns) vns1),
   12.25 -	   Bound(allargs_cnt+0)===mk_cfapp(%%con,map (bound_arg allvns) vns2)));
   12.26 +	   Bound(allargs_cnt+1)===mk_cRep_CFun(%%con,map (bound_arg allvns) vns1),
   12.27 +	   Bound(allargs_cnt+0)===mk_cRep_CFun(%%con,map (bound_arg allvns) vns2)));
   12.28          in foldr mk_ex (allvns, foldr mk_conj 
   12.29  			      (map (defined o Bound) nonlazy_idxs,capps)) end;
   12.30        fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp(
    13.1 --- a/src/HOLCF/domain/library.ML	Mon Aug 10 17:06:02 1998 +0200
    13.2 +++ b/src/HOLCF/domain/library.ML	Wed Aug 12 12:17:20 1998 +0200
    13.3 @@ -145,11 +145,11 @@
    13.4  infix 1 <<;  fun S <<  T = %%"op <<" $ S $ T;
    13.5  infix 1 ~<<; fun S ~<< T = mk_not (S << T);
    13.6  
    13.7 -infix 9 `  ; fun f`  x = %%"fapp" $ f $ x;
    13.8 +infix 9 `  ; fun f`  x = %%"Rep_CFun" $ f $ x;
    13.9  infix 9 `% ; fun f`% s = f` % s;
   13.10  infix 9 `%%; fun f`%%s = f` %%s;
   13.11 -fun mk_cfapp (F,As) = foldl (op `) (F,As);
   13.12 -fun con_app2 con f args = mk_cfapp(%%con,map f args);
   13.13 +fun mk_cRep_CFun (F,As) = foldl (op `) (F,As);
   13.14 +fun con_app2 con f args = mk_cRep_CFun(%%con,map f args);
   13.15  fun con_app con = con_app2 con %#;
   13.16  fun if_rec  arg f y   = if is_rec arg then f (rec_of arg) else y;
   13.17  fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) Id (%# arg);
   13.18 @@ -166,7 +166,7 @@
   13.19  		       T (map ((fn tp => tp ->> tp) o Type o fix_tp o fst) eqs);
   13.20  fun lift tfn = foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
   13.21  
   13.22 -fun /\ v T = %%"fabs" $ mk_lam(v,T);
   13.23 +fun /\ v T = %%"Abs_CFun" $ mk_lam(v,T);
   13.24  fun /\# (arg,T) = /\ (vname arg) T;
   13.25  infixr 9 oo; fun S oo T = %%"cfcomp"`S`T;
   13.26  val UU = %%"UU";
   13.27 @@ -176,12 +176,12 @@
   13.28  fun lift_defined f = lift (fn x => defined (f x));
   13.29  fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
   13.30  
   13.31 -fun cont_eta_contract (Const("fabs",TT) $ Abs(a,T,body)) = 
   13.32 +fun cont_eta_contract (Const("Abs_CFun",TT) $ Abs(a,T,body)) = 
   13.33        (case cont_eta_contract body  of
   13.34 -        body' as (Const("fapp",Ta) $ f $ Bound 0) => 
   13.35 +        body' as (Const("Rep_CFun",Ta) $ f $ Bound 0) => 
   13.36  	  if not (0 mem loose_bnos f) then incr_boundvars ~1 f 
   13.37 -	  else   Const("fabs",TT) $ Abs(a,T,body')
   13.38 -      | body' => Const("fabs",TT) $ Abs(a,T,body'))
   13.39 +	  else   Const("Abs_CFun",TT) $ Abs(a,T,body')
   13.40 +      | body' => Const("Abs_CFun",TT) $ Abs(a,T,body'))
   13.41  |   cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t
   13.42  |   cont_eta_contract t    = t;
   13.43  
   13.44 @@ -197,7 +197,7 @@
   13.45  		in cont_eta_contract (foldr'' 
   13.46  			(fn (a,t) => %%"ssplit"`(/\# (a,t)))
   13.47  			(args,
   13.48 -			fn a=> /\#(a,(mk_cfapp(funarg(l2,n),mapn idxs 1 args))))
   13.49 +			fn a=> /\#(a,(mk_cRep_CFun(funarg(l2,n),mapn idxs 1 args))))
   13.50  			) end;
   13.51  in (if length cons = 1 andalso length(snd(hd cons)) <= 1
   13.52      then fn t => %%"strictify"`t else Id)
    14.1 --- a/src/HOLCF/domain/syntax.ML	Mon Aug 10 17:06:02 1998 +0200
    14.2 +++ b/src/HOLCF/domain/syntax.ML	Wed Aug 12 12:17:20 1998 +0200
    14.3 @@ -71,7 +71,7 @@
    14.4  					 (string_of_int m));
    14.5  	fun app s (l,r)   = mk_appl (Constant s) [l,r];
    14.6  	fun case1 n (con,mx,args) = mk_appl (Constant "@case1")
    14.7 -		 [foldl (app "fapp") (c_ast con mx, (mapn (argvar n) 1 args)),
    14.8 +		 [foldl (app "Rep_CFun") (c_ast con mx, (mapn (argvar n) 1 args)),
    14.9  		  expvar n];
   14.10  	fun arg1 n (con,_,args) = if args = [] then expvar n 
   14.11  				  else mk_appl (Constant "LAM ") 
   14.12 @@ -81,8 +81,8 @@
   14.13        (mk_appl (Constant "@case") [Variable "x", foldr'
   14.14  				(fn (c,cs) => mk_appl (Constant"@case2") [c,cs])
   14.15  				 (mapn case1 1 cons')],
   14.16 -       mk_appl (Constant "fapp") [foldl 
   14.17 -				(fn (w,a ) => mk_appl (Constant"fapp" ) [w,a ])
   14.18 +       mk_appl (Constant "Rep_CFun") [foldl 
   14.19 +				(fn (w,a ) => mk_appl (Constant"Rep_CFun" ) [w,a ])
   14.20  				 (Constant (dnam^"_when"),mapn arg1 1 cons'),
   14.21  				 Variable "x"])
   14.22    end;
    15.1 --- a/src/HOLCF/domain/theorems.ML	Mon Aug 10 17:06:02 1998 +0200
    15.2 +++ b/src/HOLCF/domain/theorems.ML	Wed Aug 12 12:17:20 1998 +0200
    15.3 @@ -41,7 +41,7 @@
    15.4                                  asm_simp_tac (HOLCF_ss addsimps rews) i;
    15.5  
    15.6  val chain_tac = REPEAT_DETERM o resolve_tac 
    15.7 -                [chain_iterate, ch2ch_fappR, ch2ch_fappL];
    15.8 +                [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL];
    15.9  
   15.10  (* ----- general proofs ----------------------------------------------------- *)
   15.11  
   15.12 @@ -175,7 +175,7 @@
   15.13  val when_apps = let fun one_when n (con,args) = pg axs_con_def 
   15.14                  (bind_fun (lift_defined % (nonlazy args, 
   15.15                  mk_trp(when_app`(con_app con args) ===
   15.16 -                       mk_cfapp(bound_fun n 0,map %# args)))))[
   15.17 +                       mk_cRep_CFun(bound_fun n 0,map %# args)))))[
   15.18                  asm_simp_tac (HOLCF_ss addsimps [when_appl,ax_abs_iso]) 1];
   15.19          in mapn one_when 1 cons end;
   15.20  end;
    16.1 --- a/src/HOLCF/ex/Hoare.ML	Mon Aug 10 17:06:02 1998 +0200
    16.2 +++ b/src/HOLCF/ex/Hoare.ML	Wed Aug 12 12:17:20 1998 +0200
    16.3 @@ -262,7 +262,7 @@
    16.4          (rtac adm_eq 1),
    16.5          (cont_tacR 1),
    16.6          (rtac allI 1),
    16.7 -        (stac strict_fapp1 1),
    16.8 +        (stac strict_Rep_CFun1 1),
    16.9          (rtac refl 1),
   16.10          (Simp_tac 1),
   16.11          (rtac allI 1),
   16.12 @@ -295,7 +295,7 @@
   16.13          (rtac adm_eq 1),
   16.14          (cont_tacR 1),
   16.15          (rtac allI 1),
   16.16 -        (stac strict_fapp1 1),
   16.17 +        (stac strict_Rep_CFun1 1),
   16.18          (rtac refl 1),
   16.19          (rtac allI 1),
   16.20          (Simp_tac 1),
   16.21 @@ -336,7 +336,7 @@
   16.22          (rtac adm_eq 1),
   16.23          (cont_tacR 1),
   16.24          (rtac allI 1),
   16.25 -        (stac strict_fapp1 1),
   16.26 +        (stac strict_Rep_CFun1 1),
   16.27          (rtac refl 1),
   16.28          (rtac allI 1),
   16.29          (Simp_tac 1),
    17.1 --- a/src/HOLCF/ex/Stream.ML	Mon Aug 10 17:06:02 1998 +0200
    17.2 +++ b/src/HOLCF/ex/Stream.ML	Wed Aug 12 12:17:20 1998 +0200
    17.3 @@ -77,7 +77,7 @@
    17.4  
    17.5  qed_goal "stream_when_strictf" thy "stream_when`UU`s=UU" (fn _ => [
    17.6  	stream_case_tac "s" 1,
    17.7 -	ALLGOALS(asm_simp_tac (HOL_ss addsimps strict_fapp1::stream.when_rews))
    17.8 +	ALLGOALS(asm_simp_tac (HOL_ss addsimps strict_Rep_CFun1::stream.when_rews))
    17.9  	]);
   17.10  	
   17.11