src/HOL/Library/BigO.thy
changeset 23373 ead82c82da9e
parent 22665 cf152ff55d16
child 23413 5caa2710dd5b
     1.1 --- a/src/HOL/Library/BigO.thy	Wed Jun 13 16:43:02 2007 +0200
     1.2 +++ b/src/HOL/Library/BigO.thy	Wed Jun 13 18:30:11 2007 +0200
     1.3 @@ -282,7 +282,7 @@
     1.4      apply (subst func_diff)
     1.5      apply (rule bigo_abs)
     1.6      done
     1.7 -  also have "... <= O(h)"
     1.8 +  also from a have "... <= O(h)"
     1.9      by (rule bigo_elt_subset)
    1.10    finally show "(%x. abs (f x) - abs (g x)) : O(h)".
    1.11  qed