fixed minor typo in comments
authoravigad
Fri, 29 Jul 2005 19:47:34 +0200
changeset 16961 9c5871b16553
parent 16960 7db2d289862a
child 16962 f99dd1274c5f
fixed minor typo in comments
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}