src/HOL/Library/Multiset.thy
changeset 38857 97775f3e8722
parent 38287 796302ca3611
child 39198 f967a16dfcdd
     1.1 --- a/src/HOL/Library/Multiset.thy	Fri Aug 27 15:36:02 2010 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Fri Aug 27 19:34:23 2010 +0200
     1.3 @@ -938,17 +938,21 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 -instantiation multiset :: (eq) eq
     1.8 +instantiation multiset :: (equal) equal
     1.9  begin
    1.10  
    1.11  definition
    1.12 -  "HOL.eq A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
    1.13 +  "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
    1.14  
    1.15  instance proof
    1.16 -qed (simp add: eq_multiset_def eq_iff)
    1.17 +qed (simp add: equal_multiset_def eq_iff)
    1.18  
    1.19  end
    1.20  
    1.21 +lemma [code nbe]:
    1.22 +  "HOL.equal (A :: 'a::equal multiset) A \<longleftrightarrow> True"
    1.23 +  by (fact equal_refl)
    1.24 +
    1.25  definition (in term_syntax)
    1.26    bagify :: "('a\<Colon>typerep \<times> nat) list \<times> (unit \<Rightarrow> Code_Evaluation.term)
    1.27      \<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where