src/HOL/Library/BigO.thy

   apply (force split: split_max)
   apply (auto split: split_max simp add: func_plus)
   done
 
 lemma bigo_LIMSEQ1: "f =o O(g) ==> g ----> 0 ==> f ----> (0::real)"
-  apply (simp add: LIMSEQ_def bigo_alt_def)
+  apply (simp add: LIMSEQ_iff bigo_alt_def)
   apply clarify
   apply (drule_tac x = "r / c" in spec)
   apply (drule mp)
   apply (erule divide_pos_pos)
   apply assumption