| changeset 45866 | e62b319c7696 |
| parent 45694 | 4a8743618257 |
| child 45989 | b39256df5f8a |
--- a/src/HOL/Library/Multiset.thy Wed Dec 14 15:05:22 2011 +0100 +++ b/src/HOL/Library/Multiset.thy Wed Dec 14 15:56:29 2011 +0100 @@ -1103,7 +1103,7 @@ begin definition - "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A" + [code]: "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A" instance proof qed (simp add: equal_multiset_def eq_iff)