diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Library/BigO.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -39,7 +39,7 @@
 subsection {* Definitions *}
 
 definition
-  bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set"    ("(1O'(_'))")
+  bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set"  ("(1O'(_'))") where
   "O(f::('a => 'b)) =
       {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
 
@@ -736,7 +736,7 @@
 
 definition
   lesso :: "('a => 'b::ordered_idom) => ('a => 'b) => ('a => 'b)"
-      (infixl "<o" 70)
+    (infixl "<o" 70) where
   "f <o g = (%x. max (f x - g x) 0)"
 
 lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==>