src/HOL/Analysis/Ball_Volume.thy
 changeset 69566 c41954ee87cf parent 69517 dc20f278e8f3 child 70136 f03a01a18c6e
```     1.1 --- a/src/HOL/Analysis/Ball_Volume.thy	Tue Jan 01 20:57:54 2019 +0100
1.2 +++ b/src/HOL/Analysis/Ball_Volume.thy	Tue Jan 01 21:47:27 2019 +0100
1.3 @@ -3,7 +3,7 @@
1.4     Author:   Manuel Eberl, TU München
1.5  *)
1.6
1.7 -section \<open>The Volume of an \$n\$-Dimensional Ball\<close>
1.8 +section \<open>The Volume of an \<open>n\<close>-Dimensional Ball\<close>
1.9
1.10  theory Ball_Volume
1.11    imports Gamma_Function Lebesgue_Integral_Substitution
1.12 @@ -25,8 +25,8 @@
1.13
1.14  text \<open>
1.15    We first need the value of the following integral, which is at the core of
1.16 -  computing the measure of an \$n+1\$-dimensional ball in terms of the measure of an
1.17 -  \$n\$-dimensional one.
1.18 +  computing the measure of an \<open>n + 1\<close>-dimensional ball in terms of the measure of an
1.19 +  \<open>n\<close>-dimensional one.
1.20  \<close>
1.21  lemma emeasure_cball_aux_integral:
1.22    "(\<integral>\<^sup>+x. indicator {-1..1} x * sqrt (1 - x\<^sup>2) ^ n \<partial>lborel) =
```