--- a/src/HOL/Library/Dlist.thy Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/Dlist.thy Fri Aug 27 19:34:23 2010 +0200
@@ -109,16 +109,20 @@
text {* Equality *}
-instantiation dlist :: (eq) eq
+instantiation dlist :: (equal) equal
begin
-definition "HOL.eq dxs dys \<longleftrightarrow> HOL.eq (list_of_dlist dxs) (list_of_dlist dys)"
+definition "HOL.equal dxs dys \<longleftrightarrow> HOL.equal (list_of_dlist dxs) (list_of_dlist dys)"
instance proof
-qed (simp add: eq_dlist_def eq list_of_dlist_inject)
+qed (simp add: equal_dlist_def equal list_of_dlist_inject)
end
+lemma [code nbe]:
+ "HOL.equal (dxs :: 'a::equal dlist) dxs \<longleftrightarrow> True"
+ by (fact equal_refl)
+
section {* Induction principle and case distinction *}