# HG changeset patch # User haftmann # Date 1404569063 -7200 # Node ID 2f640245fc6d39c2fe263000ae49ad04796fa21d # Parent f4904e2b3040bbad0c9497ad4d0159a46a276804 refrain from auxiliary abbreviation: be more explicit to the reader in situations where syntax translation does not apply; uniform appearance of xsymbol and HTML output for sums diff -r f4904e2b3040 -r 2f640245fc6d src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Sat Jul 05 12:04:25 2014 +0200 +++ b/src/HOL/Library/Multiset.thy Sat Jul 05 16:04:23 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 \ 'a) \ 'b multiset \ 'a" -where - "msetsum_image f M \ msetsum (image_mset f M)" - end syntax @@ -1218,14 +1214,14 @@ syntax (xsymbols) "_msetsum_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_add" - ("(3\_:#_. _)" [0, 51, 10] 10) + ("(3\_\#_. _)" [0, 51, 10] 10) syntax (HTML output) "_msetsum_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_add" ("(3\_\#_. _)" [0, 51, 10] 10) translations - "SUM i :# A. b" == "CONST msetsum_image (\i. b) A" + "SUM i :# A. b" == "CONST msetsum (CONST image_mset (\i. b) A)" context comm_monoid_mult begin @@ -1262,10 +1258,6 @@ "msetprod M = setprod (\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 \ 'a) \ 'b multiset \ 'a" -where - "msetprod_image f M \ msetprod (image_mset f M)" - end syntax @@ -1281,7 +1273,7 @@ ("(3\_\#_. _)" [0, 51, 10] 10) translations - "PROD i :# A. b" == "CONST msetprod_image (\i. b) A" + "PROD i :# A. b" == "CONST msetprod (CONST image_mset (\i. b) A)" lemma (in comm_semiring_1) dvd_msetprod: assumes "x \# A"