src/HOL/Map.thy
changeset 56545 8f1e7596deb7
parent 55466 786edc984c98
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Map.thy	Sat Apr 12 17:26:27 2014 +0200
     1.2 +++ b/src/HOL/Map.thy	Sat Apr 12 11:27:36 2014 +0200
     1.3 @@ -249,6 +249,10 @@
     1.4    "dom (\<lambda>k. map_option (f k) (m k)) = dom m"
     1.5    by (simp add: dom_def)
     1.6  
     1.7 +lemma dom_map_option_comp [simp]:
     1.8 +  "dom (map_option g \<circ> m) = dom m"
     1.9 +  using dom_map_option [of "\<lambda>_. g" m] by (simp add: comp_def)
    1.10 +
    1.11  
    1.12  subsection {* @{const map_option} related *}
    1.13