--- a/NEWS Mon Jan 04 21:25:40 2021 +0100
+++ b/NEWS Tue Jan 05 03:35:46 2021 +0100
@@ -169,7 +169,8 @@
division, instantiated for type int.
* Theory "Multiset": removed misleading notation \<Union># for sum_mset;
-replaced with \<Sum>\<^sub>#.
+replaced with \<Sum>\<^sub>#. Analogous notation for prod_mset also
+exists now.
* Self-contained library theory "Word" taken over from former session
"HOL-Word".
--- a/src/HOL/Library/Multiset.thy Mon Jan 04 21:25:40 2021 +0100
+++ b/src/HOL/Library/Multiset.thy Tue Jan 05 03:35:46 2021 +0100
@@ -2470,6 +2470,8 @@
end
+notation prod_mset ("\<Prod>\<^sub>#")
+
syntax (ASCII)
"_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3PROD _:#_. _)" [0, 51, 10] 10)
syntax