src/HOL/Library/Dlist.thy
changeset 40603 963ee2331d20
parent 40122 1d8ad2ff3e01
child 40672 abd4e7358847
     1.1 --- a/src/HOL/Library/Dlist.thy	Thu Nov 18 17:01:15 2010 +0100
     1.2 +++ b/src/HOL/Library/Dlist.thy	Thu Nov 18 17:01:15 2010 +0100
     1.3 @@ -173,6 +173,12 @@
     1.4  qed
     1.5  
     1.6  
     1.7 +section {* Functorial structure *}
     1.8 +
     1.9 +type_mapper map
    1.10 +  by (auto intro: dlist_eqI simp add: remdups_map_remdups comp_def)
    1.11 +
    1.12 +
    1.13  section {* Implementation of sets by distinct lists -- canonical! *}
    1.14  
    1.15  definition Set :: "'a dlist \<Rightarrow> 'a fset" where