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