src/HOL/Library/Multiset.thy

--- 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