src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
changeset 44142 8e27e0177518
parent 44125 230a8665c919
child 44167 e81d676d598e
     1.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Aug 10 17:02:03 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Aug 10 18:02:16 2011 -0700
     1.3 @@ -420,7 +420,7 @@
     1.4        using ereal_open_cont_interval2[of S f0] real lim by auto
     1.5      then have "eventually (\<lambda>x. f x \<in> {a<..<b}) net"
     1.6        unfolding Liminf_Sup Limsup_Inf less_Sup_iff Inf_less_iff
     1.7 -      by (auto intro!: eventually_conj simp add: greaterThanLessThan_iff)
     1.8 +      by (auto intro!: eventually_conj)
     1.9      with `{a<..<b} \<subseteq> S` show "eventually (%x. f x : S) net"
    1.10        by (rule_tac eventually_mono) auto
    1.11    qed
    1.12 @@ -1036,7 +1036,7 @@
    1.13    proof (rule ccontr)
    1.14      assume "\<not> ?thesis" then have "\<forall>i\<in>A. \<exists>r. f i = ereal r" by auto
    1.15      from bchoice[OF this] guess r ..
    1.16 -    with * show False by (auto simp: setsum_ereal)
    1.17 +    with * show False by auto
    1.18    qed
    1.19    ultimately show "finite A \<and> (\<exists>i\<in>A. \<bar>f i\<bar> = \<infinity>)" by auto
    1.20  next