diff -r e17f13cd1280 -r a9ed5fcc5e39 src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Thu May 28 22:57:17 2009 -0700
+++ b/src/HOL/Library/BigO.thy	Thu May 28 23:03:12 2009 -0700
@@ -871,7 +871,7 @@
   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)