# HG changeset patch
# User avigad
# Date 1122659254 -7200
# Node ID 9c5871b16553a57cf2d7f0a575e720ba31a7bf6d
# Parent  7db2d289862ae3cdb6da43828f96c57d06a80931
fixed minor typo in comments

diff -r 7db2d289862a -r 9c5871b16553 src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Fri Jul 29 19:47:27 2005 +0200
+++ b/src/HOL/Library/BigO.thy	Fri Jul 29 19:47:34 2005 +0200
@@ -24,8 +24,8 @@
 \item We have eliminated the $O$ operator on sets. (Most uses of this seem
   to be inessential.)
 \item We no longer use $+$ as output syntax for $+o$.
-\item Lemmas involving ``sumr-pos'' have been replaced by more
-  general lemmas involving ``setsum''.
+\item Lemmas involving ``sumr'' have been replaced by more general lemmas 
+  involving ``setsum''.
 \item The library has been expanded, with e.g.~support for expressions of
   the form $f < g + O(h)$.
 \end{itemize}