# HG changeset patch
# User blanchet
# Date 1671556819 -3600
# Node ID c48fe2be847f09efc9a5e8364dbf0329c399a0ef
# Parent  0b5efc6de3858af497e67fe794ce6890338f5f4c
added lifting_forget as suggested by Peter Lammich

diff -r 0b5efc6de385 -r c48fe2be847f src/HOL/Computational_Algebra/Factorial_Ring.thy
--- 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
diff -r 0b5efc6de385 -r c48fe2be847f 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