src/HOL/Probability/Radon_Nikodym.thy

     using g_in_G `incseq ?g`
     by (auto intro!: positive_integral_monotone_convergence_SUP simp: G_def)
   also have "\<dots> = ?y"
   proof (rule antisym)
     show "(SUP i. integral\<^sup>P M (?g i)) \<le> ?y"
-      using g_in_G by (auto intro: Sup_mono simp: SUP_def)
+      using g_in_G by (auto intro: SUP_mono)
     show "?y \<le> (SUP i. integral\<^sup>P M (?g i))" unfolding y_eq
       by (auto intro!: SUP_mono positive_integral_mono Max_ge)
   qed
   finally have int_f_eq_y: "integral\<^sup>P M f = ?y" .
   have "\<And>x. 0 \<le> f x"