--- a/src/Doc/Logics/document/HOL.tex Sun Oct 16 22:43:51 2016 +0200
+++ b/src/Doc/Logics/document/HOL.tex Mon Oct 17 11:46:22 2016 +0200
@@ -145,7 +145,7 @@
numbers). The type class \cldx{plus_ac0} comprises all types for which 0
and~+ satisfy the laws $x+y=y+x$, $(x+y)+z = x+(y+z)$ and $0+x = x$. These
types include the numeric ones \tdx{nat}, \tdx{int} and~\tdx{real} and also
-multisets. The summation operator \cdx{setsum} is available for all types in
+multisets. The summation operator \cdx{sum} is available for all types in
this class.
Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order