src/HOL/Analysis/ex/Circle_Area.thy
 changeset 64911 f0e07600de47 parent 64892 662de910a96b child 66453 cc19f7ca2ed6
```     1.1 --- a/src/HOL/Analysis/ex/Circle_Area.thy	Tue Jan 17 11:26:21 2017 +0100
1.2 +++ b/src/HOL/Analysis/ex/Circle_Area.thy	Tue Jan 17 13:59:10 2017 +0100
1.3 @@ -4,7 +4,7 @@
1.4  A proof that the area of a circle with radius R is R\<^sup>2\<pi>.
1.5  *)
1.6
1.7 -section {* The area of a circle *}
1.8 +section \<open>The area of a circle\<close>
1.9
1.10  theory Circle_Area
1.11  imports Complex_Main Interval_Integral
1.12 @@ -157,13 +157,13 @@
1.13    also have "... = \<integral>\<^sup>+x. R * \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel"
1.14    proof (rule nn_integral_cong)
1.15      fix x from R show "(\<integral>\<^sup>+y. indicator ?A (x,y) \<partial>lborel) = R * \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel"
1.16 -      by (subst nn_integral_real_affine[OF _ `R \<noteq> 0`, of _ 0]) simp_all
1.17 +      by (subst nn_integral_real_affine[OF _ \<open>R \<noteq> 0\<close>, of _ 0]) simp_all
1.18    qed
1.19    also have "... = R * \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel"
1.20      using R by (intro nn_integral_cmult) simp_all
1.21    also from R have "(\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel) =
1.22                          R * \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (R*x,R*y) \<partial>lborel \<partial>lborel"
1.23 -    by (subst nn_integral_real_affine[OF _ `R \<noteq> 0`, of _ 0]) simp_all
1.24 +    by (subst nn_integral_real_affine[OF _ \<open>R \<noteq> 0\<close>, of _ 0]) simp_all
1.25    also {
1.26      fix x y
1.27      have A: "(R*x, R*y) = R *\<^sub>R (x,y)" by simp
```