# HG changeset patch
# User bulwahn
# Date 1332921652 -7200
# Node ID 2fa00264392a1a5dfde0f232f1a11874c351f776
# Parent  9fc17f9ccd6c0ad96306e100c55317ad35eb82b8
using abstract code equations for proofs of code equations in Multiset

diff -r 9fc17f9ccd6c -r 2fa00264392a src/HOL/Library/Multiset.thy
--- 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)"