src/HOL/Library/Dlist.thy

--- a/src/HOL/Library/Dlist.thy	Mon Sep 27 13:28:54 2010 +0200
+++ b/src/HOL/Library/Dlist.thy	Mon Sep 27 14:13:22 2010 +0200
@@ -35,6 +35,10 @@
   "list_of_dlist (Dlist xs) = remdups xs"
   by (simp add: Dlist_def Abs_dlist_inverse)
 
+lemma remdups_list_of_dlist [simp]:
+  "remdups (list_of_dlist dxs) = list_of_dlist dxs"
+  by simp
+
 lemma Dlist_list_of_dlist [simp, code abstype]:
   "Dlist (list_of_dlist dxs) = dxs"
   by (simp add: Dlist_def list_of_dlist_inverse distinct_remdups_id)