--- a/src/HOL/Library/Dlist.thy Sun Apr 11 16:51:06 2010 +0200
+++ b/src/HOL/Library/Dlist.thy Sun Apr 11 16:51:07 2010 +0200
@@ -47,6 +47,7 @@
show "[] \<in> ?dlist" by simp
qed
+
text {* Formal, totalized constructor for @{typ "'a dlist"}: *}
definition Dlist :: "'a list \<Rightarrow> 'a dlist" where
@@ -60,7 +61,7 @@
"list_of_dlist (Dlist xs) = remdups xs"
by (simp add: Dlist_def Abs_dlist_inverse)
-lemma Dlist_list_of_dlist [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)
@@ -100,9 +101,6 @@
section {* Executable version obeying invariant *}
-code_abstype Dlist list_of_dlist
- by simp
-
lemma list_of_dlist_empty [simp, code abstract]:
"list_of_dlist empty = []"
by (simp add: empty_def)