diff -r 326f57825e1a -r 8d91a85b6d91 src/HOL/Library/BigO.thy --- a/src/HOL/Library/BigO.thy Fri Apr 08 13:31:16 2011 +0200 +++ b/src/HOL/Library/BigO.thy Fri Apr 08 13:59:28 2011 +0200 @@ -25,9 +25,6 @@ the form @{text "f < g + O(h)"}. \end{itemize} -See \verb,Complex/ex/BigO_Complex.thy, for additional lemmas that -require the \verb,HOL-Complex, logic image. - Note also since the Big O library includes rules that demonstrate set inclusion, to use the automated reasoners effectively with the library one should redeclare the theorem @{text "subsetI"} as an intro rule,