src/HOL/Datatype.thy
changeset 25511 54db9b5080b8
parent 24845 abcd15369ffa
child 25534 d0b74fdd6067
     1.1 --- a/src/HOL/Datatype.thy	Fri Nov 30 20:13:03 2007 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Fri Nov 30 20:13:05 2007 +0100
     1.3 @@ -652,11 +652,10 @@
     1.4  lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
     1.5    by (cases xo) auto
     1.6  
     1.7 -constdefs
     1.8 -  option_map :: "('a => 'b) => ('a option => 'b option)"
     1.9 -  "option_map == %f y. case y of None => None | Some x => Some (f x)"
    1.10 -
    1.11 -lemmas [code func del] = option_map_def
    1.12 +definition
    1.13 +  option_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"
    1.14 +where
    1.15 +  [code func del]: "option_map = (%f y. case y of None => None | Some x => Some (f x))"
    1.16  
    1.17  lemma option_map_None [simp, code]: "option_map f None = None"
    1.18    by (simp add: option_map_def)