src/HOL/Library/Multiset.thy

   shows "x dvd prod_mset A"
   using assms prod_mset_subset_imp_dvd [of "{#x#}" A] by simp
 
 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
   "_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
 translations