Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
less special syntax: make \<Sum> an ordinary function symbol
authornipkow
Thu, 31 Jan 2019 09:30:15 +0100
changeset 69767 d10fafeb93c0
parent 69766 76fbd806ebc5
child 69768 7e4966eaf781
child 69769 c19a32cb9625
less special syntax: make \<Sum> an ordinary function symbol
src/HOL/Groups_Big.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle