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