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/Measure_Space.thy
changeset 69164 74f1b0f10b2b
parent 68617 75129a73aca3
child 69260 0a9688695a1b 
--- a/src/HOL/Analysis/Measure_Space.thy	Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Sun Oct 21 09:39:09 2018 +0200
@@ -2589,7 +2589,7 @@
       using E \<Omega> by (subst (1 2) emeasure_restrict_space) (auto simp: sets_eq sets_eq[THEN sets_eq_imp_space_eq])
   next
     show "range (from_nat_into A) \<subseteq> E" "(\<Union>i. from_nat_into A i) = \<Omega>"
-      using A by (auto cong del: strong_SUP_cong)
+      using A by (auto cong del: SUP_cong_strong)
   next
     fix i
     have "emeasure (restrict_space M \<Omega>) (from_nat_into A i) = emeasure M (from_nat_into A i)"
isabelle