changeset 41752 | 6d19301074cf |
parent 41620 | 551eb49a6e91 |
child 43987 | 09f74fda1b1d |
1.1 --- a/src/HOL/Library/Dlist.thy Mon Jan 10 22:03:24 2011 +0100 1.2 +++ b/src/HOL/Library/Dlist.thy Tue Jan 11 14:12:37 2011 +0100 1.3 @@ -175,7 +175,7 @@ 1.4 1.5 section {* Functorial structure *} 1.6 1.7 -type_lifting map: map 1.8 +enriched_type map: map 1.9 by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff) 1.10 1.11