src/HOL/Library/BigO.thy
changeset 42285 8d91a85b6d91
parent 41865 4e8483cc2cc5
child 45270 d5b5c9259afd
     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,