# HG changeset patch
# User haftmann
# Date 1290096075 -3600
# Node ID 963ee2331d20fd7be1ab2b3ca13577abd3152fff
# Parent  91e58351111382a9af182c1bc06fb9f8406704f2
mapper for dlist type

diff -r 91e583511113 -r 963ee2331d20 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Thu Nov 18 17:01:15 2010 +0100
+++ b/src/HOL/Library/Dlist.thy	Thu Nov 18 17:01:15 2010 +0100
@@ -173,6 +173,12 @@
 qed
 
 
+section {* Functorial structure *}
+
+type_mapper map
+  by (auto intro: dlist_eqI simp add: remdups_map_remdups comp_def)
+
+
 section {* Implementation of sets by distinct lists -- canonical! *}
 
 definition Set :: "'a dlist \<Rightarrow> 'a fset" where