src/HOL/Analysis/Ball_Volume.thy
changeset 67399 eab6ce8368fa
parent 67278 c60e3d615b8c
child 67719 bffb7482faaa
     1.1 --- a/src/HOL/Analysis/Ball_Volume.thy	Wed Jan 10 15:21:49 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Ball_Volume.thy	Wed Jan 10 15:25:09 2018 +0100
     1.3 @@ -144,7 +144,7 @@
     1.4         (auto simp: mult_ac ennreal_mult' [symmetric] indicator_def intro!: nn_integral_cong)
     1.5    also have "(\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel) =
     1.6                 (\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A  
     1.7 -               \<partial>(distr lborel borel (op * (1/r))))" using \<open>r > 0\<close>
     1.8 +               \<partial>(distr lborel borel (( * ) (1/r))))" using \<open>r > 0\<close>
     1.9      by (subst nn_integral_distr)
    1.10         (auto simp: indicator_def field_simps real_sqrt_divide intro!: nn_integral_cong)
    1.11    also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) *