src/HOL/Library/BigO.thy
changeset 19736 d8d0f8f51d69
parent 19279 48b527d0331b
child 21404 eb85850d3eb7
     1.1 --- a/src/HOL/Library/BigO.thy	Sat May 27 17:42:00 2006 +0200
     1.2 +++ b/src/HOL/Library/BigO.thy	Sat May 27 17:42:02 2006 +0200
     1.3 @@ -38,10 +38,9 @@
     1.4  
     1.5  subsection {* Definitions *}
     1.6  
     1.7 -constdefs 
     1.8 -
     1.9 +definition
    1.10    bigo :: "('a => 'b::ordered_idom) => ('a => 'b) set"    ("(1O'(_'))")
    1.11 -  "O(f::('a => 'b)) == 
    1.12 +  "O(f::('a => 'b)) =
    1.13        {h. EX c. ALL x. abs (h x) <= c * abs (f x)}"
    1.14  
    1.15  lemma bigo_pos_const: "(EX (c::'a::ordered_idom). 
    1.16 @@ -735,10 +734,10 @@
    1.17  
    1.18  subsection {* Less than or equal to *}
    1.19  
    1.20 -constdefs 
    1.21 +definition
    1.22    lesso :: "('a => 'b::ordered_idom) => ('a => 'b) => ('a => 'b)"
    1.23        (infixl "<o" 70)
    1.24 -  "f <o g == (%x. max (f x - g x) 0)"
    1.25 +  "f <o g = (%x. max (f x - g x) 0)"
    1.26  
    1.27  lemma bigo_lesseq1: "f =o O(h) ==> ALL x. abs (g x) <= abs (f x) ==>
    1.28      g =o O(h)"