src/HOL/Library/Dlist.thy
changeset 37765 26bdfb7b680b
parent 37595 9591362629e3
child 38512 ed4703b416ed
     1.1 --- a/src/HOL/Library/Dlist.thy	Mon Jul 12 08:58:12 2010 +0200
     1.2 +++ b/src/HOL/Library/Dlist.thy	Mon Jul 12 08:58:13 2010 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4  text {* Formal, totalized constructor for @{typ "'a dlist"}: *}
     1.5  
     1.6  definition Dlist :: "'a list \<Rightarrow> 'a dlist" where
     1.7 -  [code del]: "Dlist xs = Abs_dlist (remdups xs)"
     1.8 +  "Dlist xs = Abs_dlist (remdups xs)"
     1.9  
    1.10  lemma distinct_list_of_dlist [simp]:
    1.11    "distinct (list_of_dlist dxs)"