summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Groups_List.thy

changeset 58152 | 6fe60a9a5bad |

parent 58101 | e7ebe5554281 |

child 58320 | 351810c45a48 |

1.1 --- a/src/HOL/Groups_List.thy Wed Sep 03 00:06:23 2014 +0200 1.2 +++ b/src/HOL/Groups_List.thy Wed Sep 03 00:06:24 2014 +0200 1.3 @@ -8,7 +8,7 @@ 1.4 begin 1.5 1.6 definition (in monoid_add) listsum :: "'a list \<Rightarrow> 'a" where 1.7 -"listsum xs = foldr plus xs 0" 1.8 + "listsum xs = foldr plus xs 0" 1.9 1.10 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*} 1.11