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/Distribution_Functions.thy
changeset 63092 a949b2a5f51d
parent 62975 1d066f6ab25d
child 63167 0909deb8059b 
--- a/src/HOL/Probability/Distribution_Functions.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Probability/Distribution_Functions.thy	Fri May 13 20:24:10 2016 +0200
@@ -64,7 +64,7 @@
   unfolding cdf_def by (rule measure_nonneg)
 
 lemma cdf_bounded: "cdf M x \<le> measure M (space M)"
-  unfolding cdf_def using assms by (intro bounded_measure)
+  unfolding cdf_def by (intro bounded_measure)
 
 lemma cdf_lim_infty:
   "((\<lambda>i. cdf M (real i)) \<longlonglongrightarrow> measure M (space M))"
isabelle