# HG changeset patch
# User huffman
# Date 1243576992 25200
# Node ID a9ed5fcc5e39a32514931986a1ba2e83b9901310
# Parent  e17f13cd1280788120aa610d595f0049fc9997b3
LIMSEQ_def -> LIMSEQ_iff

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)
diff -r e17f13cd1280 -r a9ed5fcc5e39 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- 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)"