# HG changeset patch
# User haftmann
# Date 1282125327 -7200
# Node ID ed4703b416edb6e65f90b1e879556d1f44c21fbf
# Parent  abf95b39d65cbec0eca2477709aef6d18ac48880
added equality instantiation

diff -r abf95b39d65c -r ed4703b416ed src/HOL/Library/Dlist.thy
--- 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