removed outdated text (cf. 84a3f86441eb);
authorwenzelm
Fri Apr 08 13:59:28 2011 +0200 (2011-04-08)
changeset 422858d91a85b6d91
parent 42284 326f57825e1a
child 42286 24075ad39ca2
removed outdated text (cf. 84a3f86441eb);
src/HOL/Library/BigO.thy
     1.1 --- a/src/HOL/Library/BigO.thy	Fri Apr 08 13:31:16 2011 +0200
     1.2 +++ b/src/HOL/Library/BigO.thy	Fri Apr 08 13:59:28 2011 +0200
     1.3 @@ -25,9 +25,6 @@
     1.4    the form @{text "f < g + O(h)"}.
     1.5  \end{itemize}
     1.6  
     1.7 -See \verb,Complex/ex/BigO_Complex.thy, for additional lemmas that
     1.8 -require the \verb,HOL-Complex, logic image.
     1.9 -
    1.10  Note also since the Big O library includes rules that demonstrate set
    1.11  inclusion, to use the automated reasoners effectively with the library
    1.12  one should redeclare the theorem @{text "subsetI"} as an intro rule,