LamEx.thy
changeset 445 f1c0a66284d3
parent 419 b1cd040ff5f7
child 451 586e3dc4afdb
equal deleted inserted replaced
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