----------------------------------------------------------------------
authorregensbu
Mon Nov 28 19:48:30 1994 +0100 (1994-11-28)
changeset 752b89462f9d5f1
parent 751 f0aacbcedb77
child 753 ec86863e87c8
----------------------------------------------------------------------
Committing in HOLCF
Use new translation mechanism and keyword syntax, cinfix.ML no
longer needed.
Optimized proofs in Cont.ML
Modified Files:
Cfun1.ML Cfun2.thy Cont.ML Cprod3.thy Makefile README
Sprod3.thy Tr2.thy ccc1.thy
----------------------------------------------------------------------
src/HOLCF/Cfun1.ML
src/HOLCF/Cfun2.thy
src/HOLCF/Cont.ML
src/HOLCF/Cprod3.thy
src/HOLCF/Makefile
src/HOLCF/README
src/HOLCF/Sprod3.thy
src/HOLCF/Tr2.thy
src/HOLCF/ccc1.thy
     1.1 --- a/src/HOLCF/Cfun1.ML	Fri Nov 25 11:13:55 1994 +0100
     1.2 +++ b/src/HOLCF/Cfun1.ML	Mon Nov 28 19:48:30 1994 +0100
     1.3 @@ -120,10 +120,3 @@
     1.4  	(atac 1)
     1.5  	]);
     1.6  
     1.7 -(* ------------------------------------------------------------------------ *)
     1.8 -(* load ML file cinfix.ML                                                   *)
     1.9 -(* ------------------------------------------------------------------------ *)
    1.10 -
    1.11 -
    1.12 - writeln "Reading file  cinfix.ML"; 
    1.13 -use "cinfix.ML";
     2.1 --- a/src/HOLCF/Cfun2.thy	Fri Nov 25 11:13:55 1994 +0100
     2.2 +++ b/src/HOLCF/Cfun2.thy	Mon Nov 28 19:48:30 1994 +0100
     2.3 @@ -28,12 +28,3 @@
     2.4  
     2.5  end
     2.6  
     2.7 -ML
     2.8 -
     2.9 -(* ----------------------------------------------------------------------*)
    2.10 -(* unique setup of print translation for fapp                            *)
    2.11 -(* ----------------------------------------------------------------------*)
    2.12 -
    2.13 -val print_translation = [("fapp",fapptr')];
    2.14 -
    2.15 -
     3.1 --- a/src/HOLCF/Cont.ML	Fri Nov 25 11:13:55 1994 +0100
     3.2 +++ b/src/HOLCF/Cont.ML	Mon Nov 28 19:48:30 1994 +0100
     3.3 @@ -172,8 +172,7 @@
     3.4  (* ------------------------------------------------------------------------ *)
     3.5  
     3.6  val ch2ch_MF2L = prove_goal Cont.thy 
     3.7 -"[|monofun(MF2::('a::po=>'b::po=>'c::po));\
     3.8 -\	is_chain(F)|] ==> is_chain(%i. MF2(F(i),x))"
     3.9 +"[|monofun(MF2); is_chain(F)|] ==> is_chain(%i. MF2(F(i),x))"
    3.10  (fn prems =>
    3.11  	[
    3.12  	(cut_facts_tac prems 1),
    3.13 @@ -182,8 +181,8 @@
    3.14  	]);
    3.15  
    3.16  
    3.17 -val ch2ch_MF2R = prove_goal Cont.thy "[|monofun(MF2(f)::('b::po=>'c::po));\
    3.18 -\	is_chain(Y)|] ==> is_chain(%i. MF2(f,Y(i)))"
    3.19 +val ch2ch_MF2R = prove_goal Cont.thy 
    3.20 +"[|monofun(MF2(f)); is_chain(Y)|] ==> is_chain(%i. MF2(f,Y(i)))"
    3.21  (fn prems =>
    3.22  	[
    3.23  	(cut_facts_tac prems 1),
    3.24 @@ -192,11 +191,9 @@
    3.25  	]);
    3.26  
    3.27  val ch2ch_MF2LR = prove_goal Cont.thy 
    3.28 -"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
    3.29 -\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
    3.30 -\	is_chain(F); is_chain(Y)|] ==> \
    3.31 +"[|monofun(MF2); !f.monofun(MF2(f)); is_chain(F); is_chain(Y)|] ==> \
    3.32  \  is_chain(%i. MF2(F(i))(Y(i)))"
    3.33 -(fn prems =>
    3.34 + (fn prems =>
    3.35  	[
    3.36  	(cut_facts_tac prems 1),
    3.37  	(rtac is_chainI 1),
    3.38 @@ -208,6 +205,7 @@
    3.39  	(etac (is_chainE RS spec) 1)
    3.40  	]);
    3.41  
    3.42 +
    3.43  val ch2ch_lubMF2R = prove_goal Cont.thy 
    3.44  "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
    3.45  \  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
    3.46 @@ -268,162 +266,113 @@
    3.47  	(atac 1)
    3.48  	]);
    3.49  
    3.50 -
    3.51  val ex_lubMF2 = prove_goal Cont.thy 
    3.52  "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
    3.53  \  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
    3.54  \	is_chain(F); is_chain(Y)|] ==> \
    3.55  \		lub(range(%j. lub(range(%i. MF2(F(j),Y(i)))))) =\
    3.56  \		lub(range(%i. lub(range(%j. MF2(F(j),Y(i))))))"
    3.57 -(fn prems =>
    3.58 + (fn prems =>
    3.59  	[
    3.60  	(cut_facts_tac prems 1),
    3.61  	(rtac antisym_less 1),
    3.62 -	(rtac is_lub_thelub 1),
    3.63 +	(rtac (ub_rangeI RSN (2,is_lub_thelub)) 1),
    3.64  	(etac ch2ch_lubMF2R 1),
    3.65 -	(atac 1),(atac 1),(atac 1),
    3.66 -	(rtac ub_rangeI 1),
    3.67 +	(REPEAT (atac 1)),
    3.68  	(strip_tac 1),
    3.69  	(rtac lub_mono 1),
    3.70  	((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
    3.71  	(atac 1),
    3.72  	(etac ch2ch_lubMF2L 1),
    3.73 -	(atac 1),(atac 1),(atac 1),
    3.74 +	(REPEAT (atac 1)),
    3.75  	(strip_tac 1),
    3.76  	(rtac is_ub_thelub 1),
    3.77 -	(etac ch2ch_MF2L 1),(atac 1),
    3.78 -	(rtac is_lub_thelub 1),
    3.79 +	(etac ch2ch_MF2L 1),
    3.80 +	(atac 1),
    3.81 +	(rtac (ub_rangeI RSN (2,is_lub_thelub)) 1),
    3.82  	(etac ch2ch_lubMF2L 1),
    3.83 -	(atac 1),(atac 1),(atac 1),
    3.84 -	(rtac ub_rangeI 1),
    3.85 +	(REPEAT (atac 1)),
    3.86  	(strip_tac 1),
    3.87  	(rtac lub_mono 1),
    3.88 -	(etac ch2ch_MF2L 1),(atac 1),
    3.89 +	(etac ch2ch_MF2L 1),
    3.90 +	(atac 1),
    3.91  	(etac ch2ch_lubMF2R 1),
    3.92 -	(atac 1),(atac 1),(atac 1),
    3.93 +	(REPEAT (atac 1)),
    3.94  	(strip_tac 1),
    3.95  	(rtac is_ub_thelub 1),
    3.96  	((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
    3.97  	(atac 1)
    3.98  	]);
    3.99  
   3.100 -(* ------------------------------------------------------------------------ *)
   3.101 -(* The following results are about a curried function that is continuous    *)
   3.102 -(* in both arguments                                                        *)
   3.103 -(* ------------------------------------------------------------------------ *)
   3.104  
   3.105 -val diag_lemma1 = prove_goal Cont.thy 
   3.106 -"[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
   3.107 -\ is_chain(%i. lub(range(%j. CF2(FY(j), TY(i)))))"
   3.108 - (fn prems =>
   3.109 -	[
   3.110 -	(cut_facts_tac prems 1),
   3.111 -	(rtac ch2ch_lubMF2L 1),
   3.112 -	(rtac contX2mono 1),
   3.113 -	(atac 1),
   3.114 -	(rtac allI 1),
   3.115 -	(rtac contX2mono 1),
   3.116 -	(etac spec 1),
   3.117 -	(atac 1),
   3.118 -	(atac 1)
   3.119 -	]);
   3.120 -
   3.121 -val diag_lemma2 = prove_goal Cont.thy 
   3.122 -"[|contX(CF2);is_chain(FY); is_chain(TY) |] ==>\
   3.123 -\ is_chain(%m. CF2(FY(m), TY(n::nat)))"
   3.124 - (fn prems =>
   3.125 -	[
   3.126 -	(cut_facts_tac prems 1),
   3.127 -	(etac (contX2mono RS ch2ch_MF2L) 1),
   3.128 -	(atac 1)
   3.129 -	]);
   3.130 -
   3.131 -val diag_lemma3 = prove_goal Cont.thy 
   3.132 -"[|!f.contX(CF2(f));is_chain(FY); is_chain(TY) |] ==>\
   3.133 -\ is_chain(%m. CF2(FY(n), TY(m)))"
   3.134 - (fn prems =>
   3.135 -	[
   3.136 -	(cut_facts_tac prems 1),
   3.137 -	(etac allE 1),
   3.138 -	(etac (contX2mono RS ch2ch_MF2R) 1),
   3.139 -	(atac 1)
   3.140 -	]);
   3.141 -
   3.142 -val diag_lemma4 = prove_goal Cont.thy 
   3.143 -"[|contX(CF2);!f.contX(CF2(f));is_chain(FY); is_chain(TY) |] ==>\
   3.144 -\ is_chain(%m. CF2(FY(m), TY(m)))"
   3.145 - (fn prems =>
   3.146 -	[
   3.147 -	(cut_facts_tac prems 1),
   3.148 -	(etac (contX2mono RS ch2ch_MF2LR) 1),
   3.149 -	(rtac allI 1),
   3.150 -	(etac allE 1),
   3.151 -	(etac contX2mono 1),
   3.152 -	(atac 1),
   3.153 -	(atac 1)
   3.154 -	]);
   3.155 -
   3.156 -
   3.157 -val diag_lubCF2_1 = prove_goal Cont.thy 
   3.158 -"[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
   3.159 -\ lub(range(%i. lub(range(%j. CF2(FY(j))(TY(i)))))) =\
   3.160 -\ lub(range(%i. CF2(FY(i))(TY(i))))"
   3.161 +val diag_lubMF2_1 = prove_goal Cont.thy 
   3.162 +"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
   3.163 +\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
   3.164 +\  is_chain(FY);is_chain(TY)|] ==>\
   3.165 +\ lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =\
   3.166 +\ lub(range(%i. MF2(FY(i))(TY(i))))"
   3.167   (fn prems =>
   3.168  	[
   3.169  	(cut_facts_tac prems 1),
   3.170  	(rtac antisym_less 1),
   3.171 -	(rtac is_lub_thelub 1),
   3.172 -	(etac diag_lemma1 1),
   3.173 +	(rtac (ub_rangeI RSN (2,is_lub_thelub)) 1),
   3.174 +	(etac ch2ch_lubMF2L 1),
   3.175  	(REPEAT (atac 1)),
   3.176 -	(rtac ub_rangeI 1),
   3.177  	(strip_tac 1 ),
   3.178  	(rtac lub_mono3 1),
   3.179 -	(etac diag_lemma2 1),
   3.180 +	(etac ch2ch_MF2L 1),
   3.181  	(REPEAT (atac 1)),
   3.182 -	(etac diag_lemma4 1),
   3.183 +	(etac ch2ch_MF2LR 1),
   3.184  	(REPEAT (atac 1)),
   3.185  	(rtac allI 1),
   3.186  	(res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
   3.187  	(res_inst_tac [("x","ia")] exI 1),
   3.188  	(rtac (chain_mono RS mp) 1),
   3.189 -	(etac diag_lemma3 1),
   3.190 +	(etac allE 1),
   3.191 +	(etac ch2ch_MF2R 1),
   3.192  	(REPEAT (atac 1)),
   3.193  	(hyp_subst_tac 1),
   3.194  	(res_inst_tac [("x","ia")] exI 1),
   3.195  	(rtac refl_less 1),
   3.196  	(res_inst_tac [("x","i")] exI 1),
   3.197  	(rtac (chain_mono RS mp) 1),
   3.198 -	(etac diag_lemma2 1),
   3.199 +	(etac ch2ch_MF2L 1),
   3.200  	(REPEAT (atac 1)),
   3.201  	(rtac lub_mono 1),
   3.202 -	(etac diag_lemma4 1),
   3.203 -	(REPEAT (atac 1)),
   3.204 -	(etac diag_lemma1 1),
   3.205 +	(etac ch2ch_MF2LR 1),
   3.206 +	(REPEAT(atac 1)),
   3.207 +	(etac ch2ch_lubMF2L 1),
   3.208  	(REPEAT (atac 1)),
   3.209  	(strip_tac 1 ),
   3.210  	(rtac is_ub_thelub 1),
   3.211 -	(etac diag_lemma2 1),
   3.212 -	(REPEAT (atac 1))
   3.213 +	(etac ch2ch_MF2L 1),
   3.214 +	(atac 1)
   3.215  	]);
   3.216  
   3.217 -val diag_lubCF2_2 = prove_goal Cont.thy 
   3.218 -"[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
   3.219 -\ lub(range(%j. lub(range(%i. CF2(FY(j))(TY(i)))))) =\
   3.220 -\ lub(range(%i. CF2(FY(i))(TY(i))))"
   3.221 +val diag_lubMF2_2 = prove_goal Cont.thy 
   3.222 +"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
   3.223 +\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
   3.224 +\  is_chain(FY);is_chain(TY)|] ==>\
   3.225 +\ lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =\
   3.226 +\ lub(range(%i. MF2(FY(i))(TY(i))))"
   3.227   (fn prems =>
   3.228  	[
   3.229  	(cut_facts_tac prems 1),
   3.230  	(rtac trans 1),
   3.231  	(rtac ex_lubMF2 1),
   3.232 -	(etac contX2mono 1),
   3.233 -	(rtac allI 1),
   3.234 -	(etac allE 1),
   3.235 -	(etac contX2mono 1),
   3.236  	(REPEAT (atac 1)),
   3.237 -	(rtac diag_lubCF2_1 1),
   3.238 +	(etac diag_lubMF2_1 1),
   3.239  	(REPEAT (atac 1))
   3.240  	]);
   3.241  
   3.242 +
   3.243 +
   3.244 +
   3.245 +(* ------------------------------------------------------------------------ *)
   3.246 +(* The following results are about a curried function that is continuous    *)
   3.247 +(* in both arguments                                                        *)
   3.248 +(* ------------------------------------------------------------------------ *)
   3.249 +
   3.250  val contlub_CF2 = prove_goal Cont.thy 
   3.251  "[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
   3.252  \ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i.CF2(FY(i))(TY(i))))"
   3.253 @@ -436,13 +385,16 @@
   3.254  	(rtac ((hd prems) RS contX2mono RS ch2ch_monofun) 1),
   3.255  	(atac 1),
   3.256  	(rtac trans 1),
   3.257 -	(rtac (((hd (tl prems)) RS spec RS contX2contlub) RS contlubE RS 
   3.258 -               spec RS mp RS ext RS arg_cong RS arg_cong) 1),
   3.259 +	(rtac (((hd (tl prems)) RS spec RS contX2contlub) RS contlubE RS                spec RS mp RS ext RS arg_cong RS arg_cong) 1),
   3.260  	(atac 1),
   3.261 -	(rtac diag_lubCF2_2 1),
   3.262 +	(rtac diag_lubMF2_2 1),
   3.263 +	(etac contX2mono 1),
   3.264 +	(rtac allI 1),
   3.265 +	(etac allE 1),
   3.266 +	(etac contX2mono 1),
   3.267  	(REPEAT (atac 1))
   3.268  	]);
   3.269 - 
   3.270 +
   3.271  (* ------------------------------------------------------------------------ *)
   3.272  (* The following results are about application for functions in 'a=>'b      *)
   3.273  (* ------------------------------------------------------------------------ *)
     4.1 --- a/src/HOLCF/Cprod3.thy	Fri Nov 25 11:13:55 1994 +0100
     4.2 +++ b/src/HOLCF/Cprod3.thy	Mon Nov 28 19:48:30 1994 +0100
     4.3 @@ -13,14 +13,14 @@
     4.4  arities "*" :: (pcpo,pcpo)pcpo			(* Witness cprod2.ML *)
     4.5  
     4.6  consts  
     4.7 -	"@cpair"     :: "'a => 'b => ('a*'b)" ("_#_" [101,100] 100)
     4.8 -	"cop @cpair" :: "'a -> 'b -> ('a*'b)" ("cpair")
     4.9 -					(* continuous  pairing *)
    4.10 +	cpair        :: "'a -> 'b -> ('a*'b)" (* continuous  pairing *)
    4.11  	cfst         :: "('a*'b)->'a"
    4.12  	csnd         :: "('a*'b)->'b"
    4.13  	csplit       :: "('a->'b->'c)->('a*'b)->'c"
    4.14  
    4.15 -translations "x#y" => "cpair[x][y]"
    4.16 +syntax	"@cpair"     :: "'a => 'b => ('a*'b)" ("_#_" [101,100] 100)
    4.17 +
    4.18 +translations "x#y" == "cpair[x][y]"
    4.19  
    4.20  rules 
    4.21  
     5.1 --- a/src/HOLCF/Makefile	Fri Nov 25 11:13:55 1994 +0100
     5.2 +++ b/src/HOLCF/Makefile	Mon Nov 28 19:48:30 1994 +0100
     5.3 @@ -20,7 +20,7 @@
     5.4  	Porder0.thy Porder.thy Porder.ML  Pcpo.thy \
     5.5  	Pcpo.ML Fun1.thy Fun1.ML Fun2.thy Fun2.ML Fun3.thy Fun3.ML \
     5.6  	Cfun1.thy Cfun1.ML Cfun2.thy Cfun2.ML Cfun3.thy Cfun3.ML \
     5.7 -	Cont.thy Cont.ML cinfix.ML\
     5.8 +	Cont.thy Cont.ML \
     5.9  	Cprod1.thy Cprod1.ML Cprod2.thy Cprod2.ML Cprod3.thy Cprod3.ML \
    5.10  	Sprod0.thy Sprod0.ML Sprod1.thy Sprod1.ML Sprod2.thy Sprod2.ML\
    5.11  	Sprod3.thy Sprod3.ML\
     6.1 --- a/src/HOLCF/README	Fri Nov 25 11:13:55 1994 +0100
     6.2 +++ b/src/HOLCF/README	Mon Nov 28 19:48:30 1994 +0100
     6.3 @@ -4,12 +4,13 @@
     6.4  Author:     Franz Regensburger
     6.5  Copyright   1993,1994 Technische Universitaet Muenchen
     6.6  
     6.7 -Version: 1.4
     6.8 -Date: 06.10.94
     6.9 +Version: 1.5
    6.10 +Date: 14.10.94
    6.11  
    6.12  A detailed description of the entire development can be found in 
    6.13  
    6.14  [Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
    6.15                       Dissertation, Technische Universit"at M"unchen, 1994
    6.16  
    6.17 -
    6.18 +Changes:
    6.19 +14.10. New translation mechanism for continuous infixes
     7.1 --- a/src/HOLCF/Sprod3.thy	Fri Nov 25 11:13:55 1994 +0100
     7.2 +++ b/src/HOLCF/Sprod3.thy	Mon Nov 28 19:48:30 1994 +0100
     7.3 @@ -10,13 +10,14 @@
     7.4  
     7.5  arities "**" :: (pcpo,pcpo)pcpo			(* Witness sprod2.ML *)
     7.6  
     7.7 -consts
     7.8 +consts  
     7.9  	spair        :: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
    7.10  	sfst         :: "('a**'b)->'a"
    7.11  	ssnd         :: "('a**'b)->'b"
    7.12  	ssplit       :: "('a->'b->'c)->('a**'b)->'c"
    7.13  
    7.14 -syntax	"@spair"     :: "'a => 'b => ('a**'b)" ("_##_" [101,100] 100)
    7.15 +syntax  "@spair"     :: "'a => 'b => ('a**'b)" ("_##_" [101,100] 100)
    7.16 +
    7.17  translations "x##y" == "spair[x][y]"
    7.18  
    7.19  rules 
     8.1 --- a/src/HOLCF/Tr2.thy	Fri Nov 25 11:13:55 1994 +0100
     8.2 +++ b/src/HOLCF/Tr2.thy	Mon Nov 28 19:48:30 1994 +0100
     8.3 @@ -9,20 +9,19 @@
     8.4  Tr2 = Tr1 +
     8.5  
     8.6  consts
     8.7 -	"@cifte"	:: "tr=>'c=>'c=>'c"
     8.8 +	Icifte		:: "tr -> 'c -> 'c -> 'c"
     8.9 +	trand		:: "tr -> tr -> tr"
    8.10 +	tror		:: "tr -> tr -> tr"
    8.11 +        neg		:: "tr -> tr"
    8.12 +
    8.13 +syntax 	"@cifte"	:: "tr=>'c=>'c=>'c"
    8.14                               ("(3If _/ (then _/ else _) fi)" 60)
    8.15 -	"Icifte"        :: "tr->'c->'c->'c"
    8.16 -
    8.17  	"@andalso"	:: "tr => tr => tr" ("_ andalso _" [36,35] 35)
    8.18 -	"cop @andalso"	:: "tr -> tr -> tr" ("trand")
    8.19  	"@orelse"	:: "tr => tr => tr" ("_ orelse _"  [31,30] 30)
    8.20 -	"cop @orelse"	:: "tr -> tr -> tr" ("tror")
    8.21 -
    8.22 -        "neg"           :: "tr -> tr"
    8.23 -
    8.24 -translations "x andalso y" => "trand[x][y]"
    8.25 -             "x orelse y"  => "tror[x][y]"
    8.26 -             "If b then e1 else e2 fi" => "Icifte[b][e1][e2]"
    8.27 + 
    8.28 +translations "x andalso y" == "trand[x][y]"
    8.29 +             "x orelse y"  == "tror[x][y]"
    8.30 +             "If b then e1 else e2 fi" == "Icifte[b][e1][e2]"
    8.31                
    8.32  rules
    8.33  
     9.1 --- a/src/HOLCF/ccc1.thy	Fri Nov 25 11:13:55 1994 +0100
     9.2 +++ b/src/HOLCF/ccc1.thy	Mon Nov 28 19:48:30 1994 +0100
     9.3 @@ -10,13 +10,12 @@
     9.4  ccc1 = Cprod3 + Sprod3 + Ssum3 + Lift3 + Fix +
     9.5  
     9.6  consts
     9.7 -
     9.8 -	ID 		:: "'a -> 'a"
     9.9 +	ID 	:: "'a -> 'a"
    9.10 +	cfcomp	:: "('b->'c)->('a->'b)->'a->'c"
    9.11  
    9.12 -	"@oo"		:: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100)
    9.13 -	"cop @oo"	:: "('b->'c)->('a->'b)->'a->'c" ("cfcomp")
    9.14 -
    9.15 -translations "f1 oo f2" => "cfcomp[f1][f2]"
    9.16 +syntax	"@oo"	:: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100)
    9.17 +     
    9.18 +translations 	"f1 oo f2" == "cfcomp[f1][f2]"
    9.19  
    9.20  rules
    9.21