src/HOL/Map.thy
changeset 30235 58d147683393
parent 29622 2eeb09477ed3
child 30738 0842e906300c
     1.1 --- a/src/HOL/Map.thy	Tue Mar 03 17:05:18 2009 +0100
     1.2 +++ b/src/HOL/Map.thy	Wed Mar 04 10:47:20 2009 +0100
     1.3 @@ -242,17 +242,17 @@
     1.4    "map_of xs k = Some z \<Longrightarrow> P k z \<Longrightarrow> map_of (filter (split P) xs) k = Some z"
     1.5  by (induct xs) auto
     1.6  
     1.7 -lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)"
     1.8 +lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = Option.map f (map_of xs x)"
     1.9  by (induct xs) auto
    1.10  
    1.11  
    1.12 -subsection {* @{term [source] option_map} related *}
    1.13 +subsection {* @{const Option.map} related *}
    1.14  
    1.15 -lemma option_map_o_empty [simp]: "option_map f o empty = empty"
    1.16 +lemma option_map_o_empty [simp]: "Option.map f o empty = empty"
    1.17  by (rule ext) simp
    1.18  
    1.19  lemma option_map_o_map_upd [simp]:
    1.20 -  "option_map f o m(a|->b) = (option_map f o m)(a|->f b)"
    1.21 +  "Option.map f o m(a|->b) = (Option.map f o m)(a|->f b)"
    1.22  by (rule ext) simp
    1.23  
    1.24