| changeset 40968 | a6fcd305f7dc |
| parent 40605 | 0bc28f978bcf |
| child 41372 | 551eb49a6e91 |
--- a/src/HOL/Library/Mapping.thy Sun Dec 05 14:02:16 2010 +0100 +++ b/src/HOL/Library/Mapping.thy Mon Dec 06 09:19:10 2010 +0100 @@ -50,7 +50,7 @@ "lookup (map f g m) = Option.map g \<circ> lookup m \<circ> f" by (simp add: map_def) -type_mapper map +type_lifting map by (auto intro!: mapping_eqI ext simp add: Option.map.compositionality Option.map.identity)