src/HOL/Library/Fundamental_Theorem_Algebra.thy
 changeset 31337 a9ed5fcc5e39 parent 31021 53642251a04f child 32456 341c83339aeb
```     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Thu May 28 22:57:17 2009 -0700
1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Thu May 28 23:03:12 2009 -0700
1.3 @@ -306,12 +306,12 @@
1.4    from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\<lambda>n. Re (s (f n))) x"
1.5      by blast
1.6    hence  x: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Re (s (f n)) - x \<bar> < r"
1.7 -    unfolding LIMSEQ_def real_norm_def .
1.8 +    unfolding LIMSEQ_iff real_norm_def .
1.9
1.10    from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\<lambda>n. Im (s (f (g n)))) y"
1.11      by blast
1.12    hence  y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar> Im (s (f (g n))) - y \<bar> < r"
1.13 -    unfolding LIMSEQ_def real_norm_def .
1.14 +    unfolding LIMSEQ_iff real_norm_def .
1.15    let ?w = "Complex x y"
1.16    from f(1) g(1) have hs: "subseq ?h" unfolding subseq_def by auto
1.17    {fix e assume ep: "e > (0::real)"
```