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/Finite_Product_Measure.thy
changeset 69661 a03a63b81f44
parent 69631 6c3e6038e74c
child 69677 a06b204527e6
child 69685 32eeb55d4bf3 
--- a/src/HOL/Analysis/Finite_Product_Measure.thy	Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Mon Jan 14 18:35:03 2019 +0000
@@ -395,9 +395,8 @@
   apply auto []
   apply auto []
   apply simp
-  apply (subst SUP_cong[OF refl])
+  apply (subst arg_cong [of _ _ Sup, OF image_cong, OF refl])
   apply (rule sets_vimage_algebra2)
-  apply auto []
   apply (auto intro!: arg_cong2[where f=sigma_sets])
   done
isabelle