src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy

       using s by (auto simp: image_subset_iff)
     from s show "s \<le> f"
       by (subst s_eq) (auto simp: image_subset_iff le_fun_def split: split_indicator split_indicator_asm)
   qed
   then show ?thesis
-    unfolding nn_integral_def_finite by (simp cong del: SUP_cong_strong)
+    unfolding nn_integral_def_finite by (simp cong del: SUP_cong_simp)
 qed
 
 lemma nn_integral_count_space_indicator:
   assumes "NO_MATCH (UNIV::'a set) (X::'a set)"
   shows "(\<integral>\<^sup>+x. f x \<partial>count_space X) = (\<integral>\<^sup>+x. f x * indicator X x \<partial>count_space UNIV)"