1.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Aug 05 16:21:27 2014 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Aug 05 16:58:19 2014 +0200
     1.3 @@ -1125,7 +1125,7 @@
     1.4    note fin = this
     1.5    have "(\<lambda>i. ereal (real (f i))) sums (\<Sum>i. ereal (real (f i)))"
     1.6      using f
     1.7 -    by (auto intro!: summable_ereal_pos summable_sums simp: ereal_le_real_iff zero_ereal_def)
     1.8 +    by (auto intro!: summable_ereal_pos simp: ereal_le_real_iff zero_ereal_def)
     1.9    also have "\<dots> = ereal r"
    1.10      using fin r by (auto simp: ereal_real)
    1.11    finally show "\<exists>r. (\<lambda>i. real (f i)) sums r"
    1.12 @@ -1252,7 +1252,8 @@
    1.13    apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union)
    1.14    apply (drule sym)
    1.15    apply auto
    1.16 -  by (metis INF_absorb centre_in_ball)
    1.17 +  apply (metis INF_absorb centre_in_ball)
    1.18 +  done
    1.19  
    1.20  
    1.21  lemma suminf_ereal_offset_le: