summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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}