src/HOL/Map.thy
changeset 55466 786edc984c98
parent 53820 9c7e97d67b45
child 56545 8f1e7596deb7
     1.1 --- a/src/HOL/Map.thy	Fri Feb 14 07:53:45 2014 +0100
     1.2 +++ b/src/HOL/Map.thy	Fri Feb 14 07:53:46 2014 +0100
     1.3 @@ -242,21 +242,21 @@
     1.4  by (induct xs) auto
     1.5  
     1.6  lemma map_of_map:
     1.7 -  "map_of (map (\<lambda>(k, v). (k, f v)) xs) = Option.map f \<circ> map_of xs"
     1.8 +  "map_of (map (\<lambda>(k, v). (k, f v)) xs) = map_option f \<circ> map_of xs"
     1.9    by (induct xs) (auto simp add: fun_eq_iff)
    1.10  
    1.11 -lemma dom_option_map:
    1.12 -  "dom (\<lambda>k. Option.map (f k) (m k)) = dom m"
    1.13 +lemma dom_map_option:
    1.14 +  "dom (\<lambda>k. map_option (f k) (m k)) = dom m"
    1.15    by (simp add: dom_def)
    1.16  
    1.17  
    1.18 -subsection {* @{const Option.map} related *}
    1.19 +subsection {* @{const map_option} related *}
    1.20  
    1.21 -lemma option_map_o_empty [simp]: "Option.map f o empty = empty"
    1.22 +lemma map_option_o_empty [simp]: "map_option f o empty = empty"
    1.23  by (rule ext) simp
    1.24  
    1.25 -lemma option_map_o_map_upd [simp]:
    1.26 -  "Option.map f o m(a|->b) = (Option.map f o m)(a|->f b)"
    1.27 +lemma map_option_o_map_upd [simp]:
    1.28 +  "map_option f o m(a|->b) = (map_option f o m)(a|->f b)"
    1.29  by (rule ext) simp
    1.30  
    1.31