src/HOL/Library/Multiset.thy

--- a/src/HOL/Library/Multiset.thy	Thu Jun 12 16:54:28 2025 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Jun 13 17:16:38 2025 +0200
@@ -2231,6 +2231,9 @@
   finally show ?thesis by simp
 qed
 
+lemma mset_minus_list_mset: "mset(minus_list_mset xs ys) = mset xs - mset ys"
+by(induction ys) (auto)
+
 lemma mset_set_set: "distinct xs \<Longrightarrow> mset_set (set xs) = mset xs"
   by (induction xs) simp_all