# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1609814146 -3600
# Node ID c03a148110cc5505c2c5b58a168c75b6c7832ace
# Parent  6ba08ec184a15178d092900e0eaa3665602f9a12
HOL-Library.Multiset: new notation for prod_mset, consistent with sum_mset

diff -r 6ba08ec184a1 -r c03a148110cc NEWS
--- 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".
diff -r 6ba08ec184a1 -r c03a148110cc src/HOL/Library/Multiset.thy
--- 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