# HG changeset patch
# User haftmann
# Date 1748521029 -7200
# Node ID 6dc902967236b5d5e972350fce7530f021eef892
# Parent  e63593ef8b15c61c97a9f7bcc19b80ed23f70fb6
added lemma

diff -r e63593ef8b15 -r 6dc902967236 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu May 29 14:17:08 2025 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu May 29 14:17:09 2025 +0200
@@ -2171,6 +2171,10 @@
 lemma mset_map[simp]: "mset (map f xs) = image_mset f (mset xs)"
   by (induct xs) simp_all
 
+lemma mset_removeAll_eq:
+  \<open>mset (removeAll x xs) = filter_mset ((\<noteq>) x) (mset xs)\<close>
+  by (induction xs) auto
+
 global_interpretation mset_set: folding add_mset "{#}"
   defines mset_set = "folding_on.F add_mset {#}"
   by standard (simp add: fun_eq_iff)