# HG changeset patch
# User nipkow
# Date 1536844550 -7200
# Node ID d6d5fb521896d649d2e2e88800fd5581cb7d5c1c
# Parent  e86d6e869b965fd1ebcf473ee8dc2328a214840d# Parent  93546c85374a6cdfd4b3206eac9196eb78b550f5
merged

diff -r e86d6e869b96 -r d6d5fb521896 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Sep 13 11:41:39 2018 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Sep 13 15:15:50 2018 +0200
@@ -1830,7 +1830,7 @@
 lemma mset_append [simp]: "mset (xs @ ys) = mset xs + mset ys"
   by (induct xs arbitrary: ys) auto
 
-lemma mset_filter: "mset (filter P xs) = {#x \<in># mset xs. P x #}"
+lemma mset_filter[simp]: "mset (filter P xs) = {#x \<in># mset xs. P x #}"
   by (induct xs) simp_all
 
 lemma mset_rev [simp]:
@@ -1887,6 +1887,9 @@
 apply simp
 done
 
+lemma union_mset_compl[simp]: "\<forall>x. P x = (\<not> Q x) \<Longrightarrow> filter_mset P M + filter_mset Q M = M"
+by (induction M) simp_all
+
 lemma mset_compl_union: "mset [x\<leftarrow>xs. P x] + mset [x\<leftarrow>xs. \<not>P x] = mset xs"
   by (induct xs) auto