src/HOL/SEQ.thy
changeset 44568 e6f291cb5810
parent 44313 d81d57979771
child 44710 9caf6883f1f4
     1.1 --- a/src/HOL/SEQ.thy	Sat Aug 27 17:26:14 2011 +0200
     1.2 +++ b/src/HOL/SEQ.thy	Sun Aug 28 09:20:12 2011 -0700
     1.3 @@ -772,7 +772,7 @@
     1.4    have X: "!!n. X n = X 0"
     1.5      by (blast intro: const [of 0]) 
     1.6    have "X = (\<lambda>n. X 0)"
     1.7 -    by (blast intro: ext X)
     1.8 +    by (blast intro: X)
     1.9    hence "L = X 0" using tendsto_const [of "X 0" sequentially]
    1.10      by (auto intro: LIMSEQ_unique lim)
    1.11    thus ?thesis
    1.12 @@ -1144,25 +1144,4 @@
    1.13  apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs)
    1.14  done
    1.15  
    1.16 -subsection {* Legacy theorem names *}
    1.17 -
    1.18 -lemmas LIMSEQ_Zfun_iff = tendsto_Zfun_iff [where F=sequentially]
    1.19 -lemmas LIMSEQ_const = tendsto_const [where F=sequentially]
    1.20 -lemmas LIMSEQ_norm = tendsto_norm [where F=sequentially]
    1.21 -lemmas LIMSEQ_add = tendsto_add [where F=sequentially]
    1.22 -lemmas LIMSEQ_minus = tendsto_minus [where F=sequentially]
    1.23 -lemmas LIMSEQ_minus_cancel = tendsto_minus_cancel [where F=sequentially]
    1.24 -lemmas LIMSEQ_diff = tendsto_diff [where F=sequentially]
    1.25 -lemmas (in bounded_linear) LIMSEQ = tendsto [where F=sequentially]
    1.26 -lemmas (in bounded_bilinear) LIMSEQ = tendsto [where F=sequentially]
    1.27 -lemmas LIMSEQ_mult = tendsto_mult [where F=sequentially]
    1.28 -lemmas LIMSEQ_inverse = tendsto_inverse [where F=sequentially]
    1.29 -lemmas LIMSEQ_divide = tendsto_divide [where F=sequentially]
    1.30 -lemmas LIMSEQ_pow = tendsto_power [where F=sequentially]
    1.31 -lemmas LIMSEQ_setsum = tendsto_setsum [where F=sequentially]
    1.32 -lemmas LIMSEQ_setprod = tendsto_setprod [where F=sequentially]
    1.33 -lemmas LIMSEQ_norm_zero = tendsto_norm_zero_iff [where F=sequentially]
    1.34 -lemmas LIMSEQ_rabs_zero = tendsto_rabs_zero_iff [where F=sequentially]
    1.35 -lemmas LIMSEQ_imp_rabs = tendsto_rabs [where F=sequentially]
    1.36 -
    1.37  end