1.1 --- a/src/HOL/Library/Dlist.thy	Wed Apr 21 21:11:26 2010 +0200
     1.2 +++ b/src/HOL/Library/Dlist.thy	Thu Apr 22 09:30:36 2010 +0200
     1.3 @@ -47,6 +47,11 @@
     1.4    show "[] \<in> ?dlist" by simp
     1.5  qed
     1.6  
     1.7 +lemma dlist_ext:
     1.8 +  assumes "list_of_dlist xs = list_of_dlist ys"
     1.9 +  shows "xs = ys"
    1.10 +  using assms by (simp add: list_of_dlist_inject)
    1.11 +
    1.12  
    1.13  text {* Formal, totalized constructor for @{typ "'a dlist"}: *}
    1.14