| changeset 41505 | 6d19301074cf |
| parent 41372 | 551eb49a6e91 |
| child 45231 | d85a2fdc586c |
--- a/src/HOL/Library/Mapping.thy Mon Jan 10 22:03:24 2011 +0100 +++ b/src/HOL/Library/Mapping.thy Tue Jan 11 14:12:37 2011 +0100 @@ -50,7 +50,7 @@ "lookup (map f g m) = Option.map g \<circ> lookup m \<circ> f" by (simp add: map_def) -type_lifting map: map +enriched_type map: map by (simp_all add: mapping_eq_iff fun_eq_iff Option.map.compositionality Option.map.id)