src/HOL/Library/Dlist.thy
changeset 39727 5dab9549c80d
parent 39380 5a2662c1e44a
child 39915 ecf97cf3d248
     1.1 --- a/src/HOL/Library/Dlist.thy	Mon Sep 27 13:28:54 2010 +0200
     1.2 +++ b/src/HOL/Library/Dlist.thy	Mon Sep 27 14:13:22 2010 +0200
     1.3 @@ -35,6 +35,10 @@
     1.4    "list_of_dlist (Dlist xs) = remdups xs"
     1.5    by (simp add: Dlist_def Abs_dlist_inverse)
     1.6  
     1.7 +lemma remdups_list_of_dlist [simp]:
     1.8 +  "remdups (list_of_dlist dxs) = list_of_dlist dxs"
     1.9 +  by simp
    1.10 +
    1.11  lemma Dlist_list_of_dlist [simp, code abstype]:
    1.12    "Dlist (list_of_dlist dxs) = dxs"
    1.13    by (simp add: Dlist_def list_of_dlist_inverse distinct_remdups_id)