| changeset 69767 | d10fafeb93c0 |
| parent 69700 | 7a92cbec7030 |
| child 69802 | 6ec272e153f0 |
--- a/src/HOL/Groups_Big.thy Wed Jan 30 22:46:49 2019 +0100 +++ b/src/HOL/Groups_Big.thy Thu Jan 31 09:30:15 2019 +0100 @@ -534,8 +534,8 @@ sublocale sum: comm_monoid_set plus 0 defines sum = sum.F .. -abbreviation Sum ("\<Sum>_" [1000] 999) - where "\<Sum>A \<equiv> sum (\<lambda>x. x) A" +abbreviation Sum ("\<Sum>") + where "\<Sum> \<equiv> sum (\<lambda>x. x)" end