# HG changeset patch
# User nipkow
# Date 1749853330 -7200
# Node ID e2be3370ae0365a4baee0ac508aee0f0fec036cd
# Parent  32dd31062eaae89f07dba042b205469ded435eb3
make canonical homomorphism [simp]

diff -r 32dd31062eaa -r e2be3370ae03 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Jun 13 20:59:51 2025 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat Jun 14 00:22:10 2025 +0200
@@ -2231,7 +2231,7 @@
   finally show ?thesis by simp
 qed
 
-lemma mset_minus_list_mset: "mset(minus_list_mset xs ys) = mset xs - mset ys"
+lemma mset_minus_list_mset[simp]: "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"