# HG changeset patch
# User haftmann
# Date 1271921436 -7200
# Node ID 42bd879dc1b00b43b814eaca6fe4ca356b5deb55
# Parent  283c84ee7db9051e005d0628c2a1affe359a63e1
lemma dlist_ext

diff -r 283c84ee7db9 -r 42bd879dc1b0 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Wed Apr 21 21:11:26 2010 +0200
+++ b/src/HOL/Library/Dlist.thy	Thu Apr 22 09:30:36 2010 +0200
@@ -47,6 +47,11 @@
   show "[] \<in> ?dlist" by simp
 qed
 
+lemma dlist_ext:
+  assumes "list_of_dlist xs = list_of_dlist ys"
+  shows "xs = ys"
+  using assms by (simp add: list_of_dlist_inject)
+
 
 text {* Formal, totalized constructor for @{typ "'a dlist"}: *}