changeset 31337 | a9ed5fcc5e39 |
parent 29786 | 84a3f86441eb |
child 35028 | 108662d50512 |
--- 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)