changeset 55466 | 786edc984c98 |
parent 55414 | eab03e9cee8a |
child 56327 | 3e62e68fb342 |
--- a/src/HOL/Library/AList.thy Fri Feb 14 07:53:45 2014 +0100 +++ b/src/HOL/Library/AList.thy Fri Feb 14 07:53:46 2014 +0100 @@ -399,7 +399,7 @@ by (simp add: map_ran_def image_image split_def) lemma map_ran_conv: - "map_of (map_ran f al) k = Option.map (f k) (map_of al k)" + "map_of (map_ran f al) k = map_option (f k) (map_of al k)" by (induct al) auto lemma distinct_map_ran: