--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy Mon Dec 19 14:09:37 2022 +0100
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy Tue Dec 20 18:20:19 2022 +0100
@@ -11,6 +11,8 @@
"HOL-Library.Multiset"
begin
+unbundle multiset.lifting
+
subsection \<open>Irreducible and prime elements\<close>
context comm_semiring_1
@@ -2257,4 +2259,7 @@
end
+lifting_update multiset.lifting
+lifting_forget multiset.lifting
+
end
--- a/src/HOL/Library/Multiset.thy Mon Dec 19 14:09:37 2022 +0100
+++ b/src/HOL/Library/Multiset.thy Tue Dec 20 18:20:19 2022 +0100
@@ -4413,6 +4413,9 @@
lemma size_psubset: "M \<subseteq># M' \<Longrightarrow> size M < size M' \<Longrightarrow> M \<subset># M'"
using less_irrefl subset_mset_def by blast
+lifting_update multiset.lifting
+lifting_forget multiset.lifting
+
hide_const (open) wcount
end