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/Probability/Lebesgue_Measure.thy
changeset 54863 82acc20ded73
parent 54775 2d3df8633dad
child 56020 f92479477c52 
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -795,7 +795,7 @@
 
     { fix z
       from F(4)[of z] have "F i z \<le> ereal (f z)"
-        by (metis SUP_upper UNIV_I ereal_max_0 min_max.sup_absorb2 nonneg)
+        by (metis SUP_upper UNIV_I ereal_max_0 max.absorb2 nonneg)
       with F(5)[of i z] have "real (F i z) \<le> f z"
         by (cases "F i z") simp_all }
     note F_bound = this
isabelle