--- a/src/HOL/Library/Dlist.thy Wed Aug 18 11:18:24 2010 +0200
+++ b/src/HOL/Library/Dlist.thy Wed Aug 18 11:55:27 2010 +0200
@@ -15,8 +15,8 @@
qed
lemma dlist_ext:
- assumes "list_of_dlist xs = list_of_dlist ys"
- shows "xs = ys"
+ assumes "list_of_dlist dxs = list_of_dlist dys"
+ shows "dxs = dys"
using assms by (simp add: list_of_dlist_inject)
@@ -107,6 +107,19 @@
by simp
+text {* Equality *}
+
+instantiation dlist :: (eq) eq
+begin
+
+definition "HOL.eq dxs dys \<longleftrightarrow> HOL.eq (list_of_dlist dxs) (list_of_dlist dys)"
+
+instance proof
+qed (simp add: eq_dlist_def eq list_of_dlist_inject)
+
+end
+
+
section {* Induction principle and case distinction *}
lemma dlist_induct [case_names empty insert, induct type: dlist]:
@@ -283,6 +296,7 @@
end
+
hide_const (open) member fold foldr empty insert remove map filter null member length fold
end