less special syntax: make \<Sum> an ordinary function symbol
authornipkow
Thu, 31 Jan 2019 09:30:15 +0100
changeset 69783 d10fafeb93c0
parent 69782 76fbd806ebc5
child 69784 7e4966eaf781
child 69785 c19a32cb9625
less special syntax: make \<Sum> an ordinary function symbol
src/HOL/Groups_Big.thy
--- 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