src/HOL/Map.thy
changeset 60057 86fa63ce8156
parent 58889 5b7a9633cfa8
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Map.thy	Mon Apr 13 13:03:41 2015 +0200
     1.2 +++ b/src/HOL/Map.thy	Tue Apr 14 11:32:01 2015 +0200
     1.3 @@ -641,6 +641,8 @@
     1.4    ultimately show ?case by (simp only: map_of.simps ran_map_upd) simp
     1.5  qed
     1.6  
     1.7 +lemma ran_map_option: "ran (\<lambda>x. map_option f (m x)) = f ` ran m"
     1.8 +by(auto simp add: ran_def)
     1.9  
    1.10  subsection {* @{text "map_le"} *}
    1.11