src/HOL/Lim.thy
changeset 31336 e17f13cd1280
parent 31017 2c227493ea56
child 31338 d41a8ba25b67
     1.1 --- a/src/HOL/Lim.thy	Thu May 28 22:54:57 2009 -0700
     1.2 +++ b/src/HOL/Lim.thy	Thu May 28 22:57:17 2009 -0700
     1.3 @@ -700,7 +700,7 @@
     1.4      }
     1.5      then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r)" by simp
     1.6      with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> e)" by auto
     1.7 -    thus ?thesis by (unfold LIMSEQ_def, auto simp add: linorder_not_less)
     1.8 +    thus ?thesis by (unfold LIMSEQ_iff, auto simp add: linorder_not_less)
     1.9    qed
    1.10    ultimately show False by simp
    1.11  qed