src/HOL/Library/BigO.thy

--- a/src/HOL/Library/BigO.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Library/BigO.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -282,7 +282,7 @@
     apply (subst func_diff)
     apply (rule bigo_abs)
     done
-  also have "... <= O(h)"
+  also from a have "... <= O(h)"
     by (rule bigo_elt_subset)
   finally show "(%x. abs (f x) - abs (g x)) : O(h)".
 qed