| changeset 73052 | c03a148110cc |
| parent 73047 | ab9e27da0e85 |
| child 73270 | e2d03448d5b5 |
--- 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