# HG changeset patch
# User bulwahn
# Date 1323874589 -3600
# Node ID e62b319c76963b2681b5f1e289b780f2b4dd5d3a
# Parent  a8b9191609a8717f30335ae9ea004db4ba75f2e6
adding code attribute to enable evaluation of equality on multisets

diff -r a8b9191609a8 -r e62b319c7696 src/HOL/Library/Multiset.thy
--- 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)