| changeset 30235 | 58d147683393 |
| parent 27487 | c8a6ce181805 |
| child 30663 | 0b6aff7451b2 |
--- a/src/HOL/Library/AssocList.thy Tue Mar 03 17:05:18 2009 +0100 +++ b/src/HOL/Library/AssocList.thy Wed Mar 04 10:47:20 2009 +0100 @@ -429,7 +429,7 @@ subsection {* @{const map_ran} *} -lemma map_ran_conv: "map_of (map_ran f al) k = option_map (f k) (map_of al k)" +lemma map_ran_conv: "map_of (map_ran f al) k = Option.map (f k) (map_of al k)" by (induct al) auto lemma dom_map_ran: "fst ` set (map_ran f al) = fst ` set al"