--- 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)
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Thu May 28 22:57:17 2009 -0700
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Thu May 28 23:03:12 2009 -0700
@@ -306,12 +306,12 @@
from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x"
by blast
hence x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Re (s (f n)) - x \<bar> < r"
- unfolding LIMSEQ_def real_norm_def .
+ unfolding LIMSEQ_iff real_norm_def .
from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\<lambda>n. Im (s (f (g n)))) y"
by blast
hence y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Im (s (f (g n))) - y \<bar> < r"
- unfolding LIMSEQ_def real_norm_def .
+ unfolding LIMSEQ_iff real_norm_def .
let ?w = "Complex x y"
from f(1) g(1) have hs: "subseq ?h" unfolding subseq_def by auto
{fix e assume ep: "e > (0::real)"