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