author huffman Thu, 28 May 2009 23:03:12 -0700 changeset 31337 a9ed5fcc5e39 parent 31336 e17f13cd1280 child 31338 d41a8ba25b67
LIMSEQ_def -> LIMSEQ_iff
```--- 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)"```