src/HOL/Library/Multiset.thy

--- a/src/HOL/Library/Multiset.thy	Tue Dec 20 09:34:37 2022 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Dec 22 21:55:51 2022 +0100
@@ -4410,6 +4410,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