changeset 36274 | 42bd879dc1b0 |
parent 36176 | 3fe7e97ccca8 |
child 36980 | 1a4cc941171a |
--- 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"}: *}