src/HOL/Library/Extended_Real.thy
changeset 56248 67dc9549fa15
parent 56218 1c3f1f2431f9
child 56536 aefb4a8da31f
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Fri Mar 21 22:54:16 2014 +0100
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Sat Mar 22 08:37:43 2014 +0100
     1.3 @@ -1613,7 +1613,8 @@
     1.4      using `0 \<le> c` by (rule ereal_mult_left_mono)
     1.5  next
     1.6    fix y
     1.7 -  assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> c * f i \<le> y"
     1.8 +  assume "\<And>i. i \<in> UNIV \<Longrightarrow> c * f i \<le> y"
     1.9 +  then have *: "\<And>i. c * f i \<le> y" by simp
    1.10    show "c * SUPREMUM UNIV f \<le> y"
    1.11    proof (cases "0 < c \<and> c \<noteq> \<infinity>")
    1.12      case True
    1.13 @@ -1631,7 +1632,7 @@
    1.14          then have "range f = {0}"
    1.15            by auto
    1.16          with True show "c * SUPREMUM UNIV f \<le> y"
    1.17 -          using * by (auto simp: SUP_def max.absorb1)
    1.18 +          using * by auto
    1.19        next
    1.20          case False
    1.21          then obtain i where "f i \<noteq> 0"