added lifting_forget as suggested by Peter Lammich
authorblanchet
Tue, 20 Dec 2022 18:20:19 +0100
changeset 76700 c48fe2be847f
parent 76699 0b5efc6de385
child 76721 5364cdc3ec0e
added lifting_forget as suggested by Peter Lammich
src/HOL/Computational_Algebra/Factorial_Ring.thy
src/HOL/Library/Multiset.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
--- 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