Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
changeset 69546 27dae626822b
parent 69457 bea49e443909
child 69654 bc758f4f09e5 
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Sun Dec 30 10:34:56 2018 +0000
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Sun Dec 30 10:34:56 2018 +0000
@@ -2058,7 +2058,7 @@
       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:
isabelle