src/HOL/Library/Extended_Real.thy

       proof (cases "\<forall>i. f i = 0")
         case True
         then have "range f = {0}"
           by auto
         with True show "c * SUPR UNIV f \<le> y"
-          using * by (auto simp: SUP_def min_max.sup_absorb1)
+          using * by (auto simp: SUP_def max.absorb1)
       next
         case False
         then obtain i where "f i \<noteq> 0"
           by auto
         with *[of i] `c = \<infinity>` `0 \<le> f i` show ?thesis

   then show "Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A" .
   show "a + Sup A \<le> Sup ((\<lambda>x. a + x) ` A)"
   proof (cases a)
     case PInf with `A \<noteq> {}`
     show ?thesis
-      by (auto simp: image_constant min_max.sup_absorb1)
+      by (auto simp: image_constant max.absorb1)
   next
     case (real r)
     then have **: "op + (- a) ` op + a ` A = A"
       by (auto simp: image_iff ac_simps zero_ereal_def[symmetric])
     from *[of "-a" "(\<lambda>x. a + x) ` A"] real show ?thesis