src/HOL/Library/Multiset.thy
changeset 47177 2fa00264392a
parent 47143 212f7a975d49
child 47179 54b38de0620e
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Mar 28 08:25:51 2012 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Mar 28 10:00:52 2012 +0200
     1.3 @@ -1192,7 +1192,7 @@
     1.4  
     1.5  lemma single_Bag [code]:
     1.6    "{#x#} = Bag (DAList.update x 1 DAList.empty)"
     1.7 -  by (simp add: multiset_eq_iff alist.Alist_inverse impl_of_update impl_of_empty)
     1.8 +  by (simp add: multiset_eq_iff alist.Alist_inverse update_code_eqn empty_code_eqn)
     1.9  
    1.10  lemma union_Bag [code]:
    1.11    "Bag xs + Bag ys = Bag (join (\<lambda>x (n1, n2). n1 + n2) xs ys)"
    1.12 @@ -1205,7 +1205,7 @@
    1.13  
    1.14  lemma filter_Bag [code]:
    1.15    "Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
    1.16 -by (rule multiset_eqI) (simp add: count_of_filter impl_of_filter)
    1.17 +by (rule multiset_eqI) (simp add: count_of_filter filter_code_eqn)
    1.18  
    1.19  lemma mset_less_eq_Bag [code]:
    1.20    "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)"