merged

--- a/CONTRIBUTORS	Sat Jul 05 13:39:53 2014 +0200
+++ b/CONTRIBUTORS	Sat Jul 05 16:28:07 2014 +0200
@@ -10,9 +10,10 @@
   Preserve equality hypotheses in "clarify" and friends. New
   "hypsubst_thin" method configuration option.
 
-* June 2014: Florian Haftmann, TUM
-  Consolidation and generalization of facts concerning products
-  (resp. sums) on finite sets.
+* Summer 2014: Florian Haftmann, TUM
+  Consolidation and generalization of facts concerning (abelian)
+  semigroups and monoids, particularly products (resp. sums) on
+  finite sets.
 
 * June 2014: Florian Haftmann, TUM
   Internal reorganisation of the local theory / named target stack.

--- a/src/HOL/Library/Multiset.thy	Sat Jul 05 13:39:53 2014 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat Jul 05 16:28:07 2014 +0200
@@ -1206,10 +1206,6 @@
   "setsum f A = msetsum (image_mset f (multiset_of_set A))"
   by (cases "finite A") (induct A rule: finite_induct, simp_all)
 
-abbreviation msetsum_image :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b multiset \<Rightarrow> 'a"
-where
-  "msetsum_image f M \<equiv> msetsum (image_mset f M)"
-
 end
 
 syntax
@@ -1218,14 +1214,14 @@
 
 syntax (xsymbols)
   "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" 
-      ("(3\<Sum>_:#_. _)" [0, 51, 10] 10)
+      ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
 
 syntax (HTML output)
   "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" 
       ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
 
 translations
-  "SUM i :# A. b" == "CONST msetsum_image (\<lambda>i. b) A"
+  "SUM i :# A. b" == "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
 
 context comm_monoid_mult
 begin
@@ -1262,10 +1258,6 @@
   "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_of M)"
   by (simp add: Multiset.fold_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def)
 
-abbreviation msetprod_image :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b multiset \<Rightarrow> 'a"
-where
-  "msetprod_image f M \<equiv> msetprod (image_mset f M)"
-
 end
 
 syntax
@@ -1281,7 +1273,7 @@
       ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
 
 translations
-  "PROD i :# A. b" == "CONST msetprod_image (\<lambda>i. b) A"
+  "PROD i :# A. b" == "CONST msetprod (CONST image_mset (\<lambda>i. b) A)"
 
 lemma (in comm_semiring_1) dvd_msetprod:
   assumes "x \<in># A"