--- a/src/HOL/Probability/Lebesgue.thy Thu May 06 23:37:07 2010 +0200
+++ b/src/HOL/Probability/Lebesgue.thy Fri May 07 09:59:24 2010 +0200
@@ -938,17 +938,17 @@
proof safe
fix t assume t: "t \<in> space M"
{ fix m n :: nat assume "m \<le> n"
- hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding class_semiring.mul_pwr by auto
+ hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding normalizing.mul_pwr by auto
have "real (natfloor (f t * 2^m) * natfloor (2^(n-m))) \<le> real (natfloor (f t * 2 ^ n))"
apply (subst *)
- apply (subst class_semiring.mul_a)
+ apply (subst normalizing.mul_a)
apply (subst real_of_nat_le_iff)
apply (rule le_mult_natfloor)
using nonneg[OF t] by (auto intro!: mult_nonneg_nonneg)
hence "real (natfloor (f t * 2^m)) * 2^n \<le> real (natfloor (f t * 2^n)) * 2^m"
apply (subst *)
- apply (subst (3) class_semiring.mul_c)
- apply (subst class_semiring.mul_a)
+ apply (subst (3) normalizing.mul_c)
+ apply (subst normalizing.mul_a)
by (auto intro: mult_right_mono simp: natfloor_power real_of_nat_power[symmetric]) }
thus "incseq (\<lambda>n. ?u n t)" unfolding u_at_t[OF t] unfolding incseq_def
by (auto simp add: le_divide_eq divide_le_eq less_divide_eq)