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