1.1 --- a/src/HOL/Library/BigO.thy	Thu May 28 22:57:17 2009 -0700
     1.2 +++ b/src/HOL/Library/BigO.thy	Thu May 28 23:03:12 2009 -0700
     1.3 @@ -871,7 +871,7 @@
     1.4    done
     1.5  
     1.6  lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> (0::real)"
     1.7 -  apply (simp add: LIMSEQ_def bigo_alt_def)
     1.8 +  apply (simp add: LIMSEQ_iff bigo_alt_def)
     1.9    apply clarify
    1.10    apply (drule_tac x = "r / c" in spec)
    1.11    apply (drule mp)