--- a/src/HOL/Probability/Distributions.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Probability/Distributions.thy Wed Apr 02 18:35:07 2014 +0200
@@ -180,7 +180,7 @@
show "DERIV (\<lambda>x. x * exp (-x)) x :> exp (-x) - x * exp (-x)"
by (auto intro!: DERIV_intros)
show "isCont (\<lambda>x. exp (- x) - x * exp (- x)) x "
- by (intro isCont_intros isCont_exp')
+ by (intro continuous_intros)
qed fact
also have "(\<integral>x. (exp (-x)) * indicator {0 .. b} x \<partial>lborel) = - exp (- b) - - exp (- 0)"
by (rule integral_FTC_atLeastAtMost) (auto intro!: DERIV_intros)