src/HOL/Library/BigO.thy
changeset 58622 aa99568f56de
parent 57514 bdc2c6b40bf2
child 58881 b9556a055632
     1.1 --- a/src/HOL/Library/BigO.thy	Tue Oct 07 22:54:49 2014 +0200
     1.2 +++ b/src/HOL/Library/BigO.thy	Tue Oct 07 23:12:08 2014 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  This library is designed to support asymptotic ``big O'' calculations,
     1.5  i.e.~reasoning with expressions of the form $f = O(g)$ and $f = g +
     1.6  O(h)$.  An earlier version of this library is described in detail in
     1.7 -\cite{Avigad-Donnelly}.
     1.8 +@{cite "Avigad-Donnelly"}.
     1.9  
    1.10  The main changes in this version are as follows:
    1.11  \begin{itemize}