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/Distributions.thy
changeset 56536 aefb4a8da31f
parent 56381 0556204bc230
child 56571 f4635657d66f 
--- a/src/HOL/Probability/Distributions.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Probability/Distributions.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -148,7 +148,7 @@
   show "emeasure M {x\<in>space M. X x \<le> a} = ereal (if 0 \<le> a then 1 - exp (- a * l) else 0)"
     using X_distr[of a] eq_0 by (auto simp: one_ereal_def)
   show "AE x in lborel. 0 \<le> exponential_density l x "
-    by (auto simp: exponential_density_def intro!: AE_I2 mult_nonneg_nonneg)
+    by (auto simp: exponential_density_def)
 qed simp_all
 
 lemma (in prob_space) exponential_distributed_iff:
isabelle