removed outdated text (cf. 84a3f86441eb);
authorwenzelm
Fri, 08 Apr 2011 13:59:28 +0200
changeset 42285 8d91a85b6d91
parent 42284 326f57825e1a
child 42286 24075ad39ca2
removed outdated text (cf. 84a3f86441eb);
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,