src/HOL/Library/Dlist.thy
changeset 36112 7fa17a225852
parent 35688 cfe0accda6e3
child 36176 3fe7e97ccca8
     1.1 --- a/src/HOL/Library/Dlist.thy	Sun Apr 11 16:51:06 2010 +0200
     1.2 +++ b/src/HOL/Library/Dlist.thy	Sun Apr 11 16:51:07 2010 +0200
     1.3 @@ -47,6 +47,7 @@
     1.4    show "[] \<in> ?dlist" by simp
     1.5  qed
     1.6  
     1.7 +
     1.8  text {* Formal, totalized constructor for @{typ "'a dlist"}: *}
     1.9  
    1.10  definition Dlist :: "'a list \<Rightarrow> 'a dlist" where
    1.11 @@ -60,7 +61,7 @@
    1.12    "list_of_dlist (Dlist xs) = remdups xs"
    1.13    by (simp add: Dlist_def Abs_dlist_inverse)
    1.14  
    1.15 -lemma Dlist_list_of_dlist [simp]:
    1.16 +lemma Dlist_list_of_dlist [simp, code abstype]:
    1.17    "Dlist (list_of_dlist dxs) = dxs"
    1.18    by (simp add: Dlist_def list_of_dlist_inverse distinct_remdups_id)
    1.19  
    1.20 @@ -100,9 +101,6 @@
    1.21  
    1.22  section {* Executable version obeying invariant *}
    1.23  
    1.24 -code_abstype Dlist list_of_dlist
    1.25 -  by simp
    1.26 -
    1.27  lemma list_of_dlist_empty [simp, code abstract]:
    1.28    "list_of_dlist empty = []"
    1.29    by (simp add: empty_def)