1.1 --- a/src/HOL/Library/BigO.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Library/BigO.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4  subsection {* Definitions *}
     1.5  
     1.6  definition
     1.7 -  bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set"    ("(1O'(_'))")
     1.8 +  bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set"  ("(1O'(_'))") where
     1.9    "O(f::('a => 'b)) =
    1.10        {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
    1.11  
    1.12 @@ -736,7 +736,7 @@
    1.13  
    1.14  definition
    1.15    lesso :: "('a => 'b::ordered_idom) => ('a => 'b) => ('a => 'b)"
    1.16 -      (infixl "<o" 70)
    1.17 +    (infixl "<o" 70) where
    1.18    "f <o g = (%x. max (f x - g x) 0)"
    1.19  
    1.20  lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==>