--- a/src/HOL/Probability/Lebesgue_Integration.thy Sat Feb 25 09:07:39 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Sat Feb 25 09:07:41 2012 +0100
@@ -366,7 +366,7 @@
also have "\<dots> \<le> natfloor (real (u x) * 2 ^ i * 2)"
proof cases
assume "0 \<le> u x" then show ?thesis
- by (intro le_mult_natfloor) (cases "u x", auto intro!: mult_nonneg_nonneg)
+ by (intro le_mult_natfloor)
next
assume "\<not> 0 \<le> u x" then show ?thesis
by (cases "u x") (auto simp: natfloor_neg mult_nonpos_nonneg)