removed outdated text (cf. 84a3f86441eb);
--- 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,