lemma remdups_list_of_dlist
authorhaftmann
Mon Sep 27 14:13:22 2010 +0200 (2010-09-27)
changeset 397275dab9549c80d
parent 39726 ba01ecc2252a
child 39728 832c42be723e
lemma remdups_list_of_dlist
src/HOL/Library/Dlist.thy
     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)