src/HOL/Library/Dlist.thy
changeset 40968 a6fcd305f7dc
parent 40672 abd4e7358847
child 41372 551eb49a6e91
     1.1 --- a/src/HOL/Library/Dlist.thy	Sun Dec 05 14:02:16 2010 +0100
     1.2 +++ b/src/HOL/Library/Dlist.thy	Mon Dec 06 09:19:10 2010 +0100
     1.3 @@ -175,7 +175,7 @@
     1.4  
     1.5  section {* Functorial structure *}
     1.6  
     1.7 -type_mapper map
     1.8 +type_lifting map
     1.9    by (auto intro: dlist_eqI simp add: remdups_map_remdups comp_def)
    1.10  
    1.11