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