adding code attribute to enable evaluation of equality on multisets
authorbulwahn
Wed Dec 14 15:56:29 2011 +0100 (2011-12-14)
changeset 45866e62b319c7696
parent 45864 a8b9191609a8
child 45867 bce0a2089dfb
adding code attribute to enable evaluation of equality on multisets
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Dec 14 15:05:22 2011 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Dec 14 15:56:29 2011 +0100
     1.3 @@ -1103,7 +1103,7 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
     1.8 +  [code]: "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
     1.9  
    1.10  instance proof
    1.11  qed (simp add: equal_multiset_def eq_iff)