--- a/src/HOL/Library/Multiset.thy Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/Multiset.thy Fri Aug 27 19:34:23 2010 +0200
@@ -938,17 +938,21 @@
qed
qed
-instantiation multiset :: (eq) eq
+instantiation multiset :: (equal) equal
begin
definition
- "HOL.eq A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
+ "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
instance proof
-qed (simp add: eq_multiset_def eq_iff)
+qed (simp add: equal_multiset_def eq_iff)
end
+lemma [code nbe]:
+ "HOL.equal (A :: 'a::equal multiset) A \<longleftrightarrow> True"
+ by (fact equal_refl)
+
definition (in term_syntax)
bagify :: "('a\<Colon>typerep \<times> nat) list \<times> (unit \<Rightarrow> Code_Evaluation.term)
\<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where