author | huffman |
Wed, 02 Mar 2005 22:57:08 +0100 | |
changeset 15563 | 9e125b675253 |
parent 15353 | b53b89d3bf03 |
permissions | -rw-r--r-- |
9245 | 1 |
(* Title: HOLCF/Cprod3 |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
1461 | 3 |
Author: Franz Regensburger |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
|
9245 | 5 |
Class instance of * for class pcpo and cpo. |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
6 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
7 |
|
2640 | 8 |
(* for compatibility with old HOLCF-Version *) |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
9 |
Goal "UU = (UU,UU)"; |
9245 | 10 |
by (simp_tac (HOL_ss addsimps [UU_def,UU_cprod_def]) 1); |
11 |
qed "inst_cprod_pcpo"; |
|
2640 | 12 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
13 |
(* ------------------------------------------------------------------------ *) |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
14 |
(* continuity of (_,_) , fst, snd *) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
15 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
16 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
17 |
Goal |
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
18 |
"chain(Y::(nat=>'a::cpo)) ==>\ |
2840
7e03e61612b0
generalized theorems and class instances for Cprod.
slotosch
parents:
2640
diff
changeset
|
19 |
\ (lub(range(Y)),(x::'b::cpo)) =\ |
9245 | 20 |
\ (lub(range(%i. fst(Y i,x))),lub(range(%i. snd(Y i,x))))"; |
21 |
by (res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1); |
|
22 |
by (rtac lub_equal 1); |
|
23 |
by (atac 1); |
|
24 |
by (rtac (monofun_fst RS ch2ch_monofun) 1); |
|
25 |
by (rtac ch2ch_fun 1); |
|
26 |
by (rtac (monofun_pair1 RS ch2ch_monofun) 1); |
|
27 |
by (atac 1); |
|
28 |
by (rtac allI 1); |
|
29 |
by (Simp_tac 1); |
|
30 |
by (rtac sym 1); |
|
31 |
by (Simp_tac 1); |
|
32 |
by (rtac (lub_const RS thelubI) 1); |
|
33 |
qed "Cprod3_lemma1"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
34 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
35 |
Goal "contlub(Pair)"; |
9245 | 36 |
by (rtac contlubI 1); |
37 |
by (strip_tac 1); |
|
38 |
by (rtac (expand_fun_eq RS iffD2) 1); |
|
39 |
by (strip_tac 1); |
|
40 |
by (stac (lub_fun RS thelubI) 1); |
|
41 |
by (etac (monofun_pair1 RS ch2ch_monofun) 1); |
|
42 |
by (rtac trans 1); |
|
43 |
by (rtac (thelub_cprod RS sym) 2); |
|
44 |
by (rtac ch2ch_fun 2); |
|
45 |
by (etac (monofun_pair1 RS ch2ch_monofun) 2); |
|
46 |
by (etac Cprod3_lemma1 1); |
|
47 |
qed "contlub_pair1"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
48 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
49 |
Goal |
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
50 |
"chain(Y::(nat=>'a::cpo)) ==>\ |
2840
7e03e61612b0
generalized theorems and class instances for Cprod.
slotosch
parents:
2640
diff
changeset
|
51 |
\ ((x::'b::cpo),lub(range Y)) =\ |
9245 | 52 |
\ (lub(range(%i. fst(x,Y i))),lub(range(%i. snd(x, Y i))))"; |
53 |
by (res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1); |
|
54 |
by (rtac sym 1); |
|
55 |
by (Simp_tac 1); |
|
56 |
by (rtac (lub_const RS thelubI) 1); |
|
57 |
by (rtac lub_equal 1); |
|
58 |
by (atac 1); |
|
59 |
by (rtac (monofun_snd RS ch2ch_monofun) 1); |
|
60 |
by (rtac (monofun_pair2 RS ch2ch_monofun) 1); |
|
61 |
by (atac 1); |
|
62 |
by (rtac allI 1); |
|
63 |
by (Simp_tac 1); |
|
64 |
qed "Cprod3_lemma2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
65 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
66 |
Goal "contlub(Pair(x))"; |
9245 | 67 |
by (rtac contlubI 1); |
68 |
by (strip_tac 1); |
|
69 |
by (rtac trans 1); |
|
70 |
by (rtac (thelub_cprod RS sym) 2); |
|
71 |
by (etac (monofun_pair2 RS ch2ch_monofun) 2); |
|
72 |
by (etac Cprod3_lemma2 1); |
|
73 |
qed "contlub_pair2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
74 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
75 |
Goal "cont(Pair)"; |
9245 | 76 |
by (rtac monocontlub2cont 1); |
77 |
by (rtac monofun_pair1 1); |
|
78 |
by (rtac contlub_pair1 1); |
|
79 |
qed "cont_pair1"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
80 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
81 |
Goal "cont(Pair(x))"; |
9245 | 82 |
by (rtac monocontlub2cont 1); |
83 |
by (rtac monofun_pair2 1); |
|
84 |
by (rtac contlub_pair2 1); |
|
85 |
qed "cont_pair2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
86 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
87 |
Goal "contlub(fst)"; |
9245 | 88 |
by (rtac contlubI 1); |
89 |
by (strip_tac 1); |
|
90 |
by (stac (lub_cprod RS thelubI) 1); |
|
91 |
by (atac 1); |
|
92 |
by (Simp_tac 1); |
|
93 |
qed "contlub_fst"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
94 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
95 |
Goal "contlub(snd)"; |
9245 | 96 |
by (rtac contlubI 1); |
97 |
by (strip_tac 1); |
|
98 |
by (stac (lub_cprod RS thelubI) 1); |
|
99 |
by (atac 1); |
|
100 |
by (Simp_tac 1); |
|
101 |
qed "contlub_snd"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
102 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
103 |
Goal "cont(fst)"; |
9245 | 104 |
by (rtac monocontlub2cont 1); |
105 |
by (rtac monofun_fst 1); |
|
106 |
by (rtac contlub_fst 1); |
|
107 |
qed "cont_fst"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
108 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
109 |
Goal "cont(snd)"; |
9245 | 110 |
by (rtac monocontlub2cont 1); |
111 |
by (rtac monofun_snd 1); |
|
112 |
by (rtac contlub_snd 1); |
|
113 |
qed "cont_snd"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
114 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
115 |
(* |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
116 |
-------------------------------------------------------------------------- |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
117 |
more lemmas for Cprod3.thy |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
118 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
119 |
-------------------------------------------------------------------------- |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
120 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
121 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
122 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
123 |
(* convert all lemmas to the continuous versions *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
124 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
125 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
126 |
Goalw [cpair_def] |
10834 | 127 |
"(LAM x y.(x,y))$a$b = (a,b)"; |
9245 | 128 |
by (stac beta_cfun 1); |
129 |
by (simp_tac (simpset() addsimps [cont_pair1,cont_pair2,cont2cont_CF1L]) 1); |
|
130 |
by (stac beta_cfun 1); |
|
131 |
by (rtac cont_pair2 1); |
|
132 |
by (rtac refl 1); |
|
133 |
qed "beta_cfun_cprod"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
134 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
135 |
Goalw [cpair_def] |
15353 | 136 |
" <a,b> = <aa,ba> ==> a=aa & b=ba"; |
9245 | 137 |
by (dtac (beta_cfun_cprod RS subst) 1); |
138 |
by (dtac (beta_cfun_cprod RS subst) 1); |
|
139 |
by (etac Pair_inject 1); |
|
140 |
by (fast_tac HOL_cs 1); |
|
141 |
qed "inject_cpair"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
142 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
143 |
Goalw [cpair_def] "UU = <UU,UU>"; |
9245 | 144 |
by (rtac sym 1); |
145 |
by (rtac trans 1); |
|
146 |
by (rtac beta_cfun_cprod 1); |
|
147 |
by (rtac sym 1); |
|
148 |
by (rtac inst_cprod_pcpo 1); |
|
149 |
qed "inst_cprod_pcpo2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
150 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
151 |
Goal |
9245 | 152 |
"<a,b> = UU ==> a = UU & b = UU"; |
153 |
by (dtac (inst_cprod_pcpo2 RS subst) 1); |
|
154 |
by (etac inject_cpair 1); |
|
155 |
qed "defined_cpair_rev"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
156 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
157 |
Goalw [cpair_def] |
9245 | 158 |
"? a b. z=<a,b>"; |
159 |
by (rtac PairE 1); |
|
160 |
by (rtac exI 1); |
|
161 |
by (rtac exI 1); |
|
162 |
by (etac (beta_cfun_cprod RS ssubst) 1); |
|
163 |
qed "Exh_Cprod2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
164 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
165 |
val prems = Goalw [cpair_def] "[|!!x y. [|p=<x,y> |] ==> Q|] ==> Q"; |
9245 | 166 |
by (rtac PairE 1); |
167 |
by (resolve_tac prems 1); |
|
168 |
by (etac (beta_cfun_cprod RS ssubst) 1); |
|
169 |
qed "cprodE"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
170 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
171 |
Goalw [cfst_def,cpair_def] |
15353 | 172 |
"cfst$<x,y> = x"; |
9245 | 173 |
by (stac beta_cfun_cprod 1); |
174 |
by (stac beta_cfun 1); |
|
175 |
by (rtac cont_fst 1); |
|
176 |
by (Simp_tac 1); |
|
177 |
qed "cfst2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
178 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
179 |
Goalw [csnd_def,cpair_def] |
15353 | 180 |
"csnd$<x,y> = y"; |
9245 | 181 |
by (stac beta_cfun_cprod 1); |
182 |
by (stac beta_cfun 1); |
|
183 |
by (rtac cont_snd 1); |
|
184 |
by (Simp_tac 1); |
|
185 |
qed "csnd2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
186 |
|
10834 | 187 |
Goal "cfst$UU = UU"; |
9245 | 188 |
by (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,cfst2]) 1); |
189 |
qed "cfst_strict"; |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
190 |
|
10834 | 191 |
Goal "csnd$UU = UU"; |
9245 | 192 |
by (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,csnd2]) 1); |
193 |
qed "csnd_strict"; |
|
2444 | 194 |
|
10834 | 195 |
Goalw [cfst_def,csnd_def,cpair_def] "<cfst$p , csnd$p> = p"; |
9245 | 196 |
by (stac beta_cfun_cprod 1); |
197 |
by (stac beta_cfun 1); |
|
198 |
by (rtac cont_snd 1); |
|
199 |
by (stac beta_cfun 1); |
|
200 |
by (rtac cont_fst 1); |
|
201 |
by (rtac (surjective_pairing RS sym) 1); |
|
202 |
qed "surjective_pairing_Cprod2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
203 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
204 |
Goalw [cfst_def,csnd_def,cpair_def] |
9245 | 205 |
"<xa,ya> << <x,y> ==> xa<<x & ya << y"; |
206 |
by (rtac less_cprod4c 1); |
|
207 |
by (dtac (beta_cfun_cprod RS subst) 1); |
|
208 |
by (dtac (beta_cfun_cprod RS subst) 1); |
|
209 |
by (atac 1); |
|
210 |
qed "less_cprod5c"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
211 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
212 |
Goalw [cfst_def,csnd_def,cpair_def] |
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
213 |
"[|chain(S)|] ==> range(S) <<| \ |
10834 | 214 |
\ <(lub(range(%i. cfst$(S i)))) , lub(range(%i. csnd$(S i)))>"; |
9245 | 215 |
by (stac beta_cfun_cprod 1); |
216 |
by (stac (beta_cfun RS ext) 1); |
|
217 |
by (rtac cont_snd 1); |
|
218 |
by (stac (beta_cfun RS ext) 1); |
|
219 |
by (rtac cont_fst 1); |
|
220 |
by (rtac lub_cprod 1); |
|
221 |
by (atac 1); |
|
222 |
qed "lub_cprod2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
223 |
|
1779 | 224 |
bind_thm ("thelub_cprod2", lub_cprod2 RS thelubI); |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
225 |
(* |
4721
c8a8482a8124
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents:
4098
diff
changeset
|
226 |
chain ?S1 ==> |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
227 |
lub (range ?S1) = |
10834 | 228 |
<lub (range (%i. cfst$(?S1 i))), lub (range (%i. csnd$(?S1 i)))>" |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
899
diff
changeset
|
229 |
*) |
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
230 |
Goalw [csplit_def] |
10834 | 231 |
"csplit$f$<x,y> = f$x$y"; |
9245 | 232 |
by (stac beta_cfun 1); |
233 |
by (Simp_tac 1); |
|
234 |
by (simp_tac (simpset() addsimps [cfst2,csnd2]) 1); |
|
235 |
qed "csplit2"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
236 |
|
9248
e1dee89de037
massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents:
9245
diff
changeset
|
237 |
Goalw [csplit_def] |
10834 | 238 |
"csplit$cpair$z=z"; |
9245 | 239 |
by (stac beta_cfun 1); |
240 |
by (Simp_tac 1); |
|
241 |
by (simp_tac (simpset() addsimps [surjective_pairing_Cprod2]) 1); |
|
242 |
qed "csplit3"; |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
243 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
244 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
245 |
(* install simplifier for Cprod *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
246 |
(* ------------------------------------------------------------------------ *) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
247 |
|
1267 | 248 |
Addsimps [cfst2,csnd2,csplit2]; |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
249 |
|
1274 | 250 |
val Cprod_rews = [cfst2,csnd2,csplit2]; |