changeset 445 | f1c0a66284d3 |
parent 419 | b1cd040ff5f7 |
child 451 | 586e3dc4afdb |
444:75af61f32ece | 445:f1c0a66284d3 |
---|---|
260 |
260 |
261 |
261 |
262 |
262 |
263 |
263 |
264 (* Construction Site code *) |
264 (* Construction Site code *) |
265 |
|
266 |
|
267 |
|
268 |
|
269 |
|
270 |
|
271 |
265 |
272 |
266 |
273 fun |
267 fun |
274 option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)" |
268 option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)" |
275 where |
269 where |