Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
make canonical homomorphism [simp]
authornipkow
Sat, 14 Jun 2025 00:22:10 +0200
changeset 82703 e2be3370ae03
parent 82702 32dd31062eaa
child 82704 e0fb46018187
make canonical homomorphism [simp]
src/HOL/Library/Multiset.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle