src/HOL/Library/BigO.thy
changeset 21404 eb85850d3eb7
parent 19736 d8d0f8f51d69
child 22665 cf152ff55d16
--- 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) ==>