--- a/src/HOL/Library/Multiset.thy Wed Mar 28 08:25:51 2012 +0200
+++ b/src/HOL/Library/Multiset.thy Wed Mar 28 10:00:52 2012 +0200
@@ -1192,7 +1192,7 @@
lemma single_Bag [code]:
"{#x#} = Bag (DAList.update x 1 DAList.empty)"
- by (simp add: multiset_eq_iff alist.Alist_inverse impl_of_update impl_of_empty)
+ by (simp add: multiset_eq_iff alist.Alist_inverse update_code_eqn empty_code_eqn)
lemma union_Bag [code]:
"Bag xs + Bag ys = Bag (join (\<lambda>x (n1, n2). n1 + n2) xs ys)"
@@ -1205,7 +1205,7 @@
lemma filter_Bag [code]:
"Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
-by (rule multiset_eqI) (simp add: count_of_filter impl_of_filter)
+by (rule multiset_eqI) (simp add: count_of_filter filter_code_eqn)
lemma mset_less_eq_Bag [code]:
"Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"