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,