src/HOL/Library/Dlist.thy
changeset 38857 97775f3e8722
parent 38512 ed4703b416ed
child 39380 5a2662c1e44a
     1.1 --- a/src/HOL/Library/Dlist.thy	Fri Aug 27 15:36:02 2010 +0200
     1.2 +++ b/src/HOL/Library/Dlist.thy	Fri Aug 27 19:34:23 2010 +0200
     1.3 @@ -109,16 +109,20 @@
     1.4  
     1.5  text {* Equality *}
     1.6  
     1.7 -instantiation dlist :: (eq) eq
     1.8 +instantiation dlist :: (equal) equal
     1.9  begin
    1.10  
    1.11 -definition "HOL.eq dxs dys \<longleftrightarrow> HOL.eq (list_of_dlist dxs) (list_of_dlist dys)"
    1.12 +definition "HOL.equal dxs dys \<longleftrightarrow> HOL.equal (list_of_dlist dxs) (list_of_dlist dys)"
    1.13  
    1.14  instance proof
    1.15 -qed (simp add: eq_dlist_def eq list_of_dlist_inject)
    1.16 +qed (simp add: equal_dlist_def equal list_of_dlist_inject)
    1.17  
    1.18  end
    1.19  
    1.20 +lemma [code nbe]:
    1.21 +  "HOL.equal (dxs :: 'a::equal dlist) dxs \<longleftrightarrow> True"
    1.22 +  by (fact equal_refl)
    1.23 +
    1.24  
    1.25  section {* Induction principle and case distinction *}
    1.26