author wenzelm Tue Jan 17 13:59:10 2017 +0100 (2017-01-17) changeset 64911 f0e07600de47 parent 64910 6108dddad9f0 child 64912 68f0465d956b
isabelle update_cartouches -c -t;
 src/HOL/Analysis/Bochner_Integration.thy file | annotate | diff | revisions src/HOL/Analysis/Borel_Space.thy file | annotate | diff | revisions src/HOL/Analysis/Brouwer_Fixpoint.thy file | annotate | diff | revisions src/HOL/Analysis/Function_Topology.thy file | annotate | diff | revisions src/HOL/Analysis/Further_Topology.thy file | annotate | diff | revisions src/HOL/Analysis/Henstock_Kurzweil_Integration.thy file | annotate | diff | revisions src/HOL/Analysis/Measure_Space.thy file | annotate | diff | revisions src/HOL/Analysis/Path_Connected.thy file | annotate | diff | revisions src/HOL/Analysis/Radon_Nikodym.thy file | annotate | diff | revisions src/HOL/Analysis/Set_Integral.thy file | annotate | diff | revisions src/HOL/Analysis/Tagged_Division.thy file | annotate | diff | revisions src/HOL/Analysis/Topology_Euclidean_Space.thy file | annotate | diff | revisions src/HOL/Analysis/ex/Circle_Area.thy file | annotate | diff | revisions src/HOL/Library/Bourbaki_Witt_Fixpoint.thy file | annotate | diff | revisions src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy file | annotate | diff | revisions src/HOL/Library/Multiset.thy file | annotate | diff | revisions src/HOL/Library/Perm.thy file | annotate | diff | revisions src/HOL/Library/Polynomial_FPS.thy file | annotate | diff | revisions src/HOL/Library/Polynomial_Factorial.thy file | annotate | diff | revisions src/HOL/Number_Theory/Euclidean_Algorithm.thy file | annotate | diff | revisions src/HOL/Number_Theory/Primes.thy file | annotate | diff | revisions src/HOL/Number_Theory/Quadratic_Reciprocity.thy file | annotate | diff | revisions
     1.1 --- a/src/HOL/Analysis/Bochner_Integration.thy	Tue Jan 17 11:26:21 2017 +0100
1.2 +++ b/src/HOL/Analysis/Bochner_Integration.thy	Tue Jan 17 13:59:10 2017 +0100
1.3 @@ -1931,9 +1931,9 @@
1.4      integral\<^sup>L M f \<le> integral\<^sup>L M g"
1.5    by (intro integral_mono_AE) auto
1.6
1.7 -text {*The next two statements are useful to bound Lebesgue integrals, as they avoid one
1.8 +text \<open>The next two statements are useful to bound Lebesgue integrals, as they avoid one
1.9  integrability assumption. The price to pay is that the upper function has to be nonnegative,
1.10 -but this is often true and easy to check in computations.*}
1.11 +but this is often true and easy to check in computations.\<close>
1.12
1.13  lemma integral_mono_AE':
1.14    fixes f::"_ \<Rightarrow> real"
1.15 @@ -2047,20 +2047,20 @@
1.16    shows "(emeasure M) {x\<in>space M. u x \<ge> c} \<le> (1/c) * (\<integral>x. u x \<partial>M)"
1.17  proof -
1.18    have "(\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M) \<le> (\<integral>\<^sup>+ x. u x \<partial>M)"
1.19 -    by (rule nn_integral_mono_AE, auto simp add: c>0 less_eq_real_def)
1.20 +    by (rule nn_integral_mono_AE, auto simp add: \<open>c>0\<close> less_eq_real_def)
1.21    also have "... = (\<integral>x. u x \<partial>M)"
1.22      by (rule nn_integral_eq_integral, auto simp add: assms)
1.23    finally have *: "(\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M) \<le> (\<integral>x. u x \<partial>M)"
1.24      by simp
1.25
1.26    have "{x \<in> space M. u x \<ge> c} = {x \<in> space M. ennreal(1/c) * u x \<ge> 1} \<inter> (space M)"
1.27 -    using c>0 by (auto simp: ennreal_mult'[symmetric])
1.28 +    using \<open>c>0\<close> by (auto simp: ennreal_mult'[symmetric])
1.29    then have "emeasure M {x \<in> space M. u x \<ge> c} = emeasure M ({x \<in> space M. ennreal(1/c) * u x \<ge> 1} \<inter> (space M))"
1.30      by simp
1.31    also have "... \<le> ennreal(1/c) * (\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M)"
1.32      by (rule nn_integral_Markov_inequality) (auto simp add: assms)
1.33    also have "... \<le> ennreal(1/c) * (\<integral>x. u x \<partial>M)"
1.34 -    apply (rule mult_left_mono) using * c>0 by auto
1.35 +    apply (rule mult_left_mono) using * \<open>c>0\<close> by auto
1.36    finally show ?thesis
1.37      using \<open>0<c\<close> by (simp add: ennreal_mult'[symmetric])
1.38  qed
1.39 @@ -2121,8 +2121,8 @@
1.40    then show ?thesis using Lim_null by auto
1.41  qed
1.42
1.43 -text {*The next lemma asserts that, if a sequence of functions converges in $L^1$, then
1.44 -it admits a subsequence that converges almost everywhere.*}
1.45 +text \<open>The next lemma asserts that, if a sequence of functions converges in $L^1$, then
1.46 +it admits a subsequence that converges almost everywhere.\<close>
1.47
1.48  lemma tendsto_L1_AE_subseq:
1.49    fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
1.50 @@ -2146,8 +2146,8 @@
1.51    have "subseq r" unfolding r_def using r0(1) by (simp add: subseq_Suc_iff)
1.52    have I: "(\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M) < ennreal((1/2)^n)" for n
1.53    proof -
1.54 -    have "r0 n \<ge> n" using subseq r0 by (simp add: seq_suble)
1.55 -    have "(1/2::real)^(r0 n) \<le> (1/2)^n" by (rule power_decreasing[OF r0 n \<ge> n], auto)
1.56 +    have "r0 n \<ge> n" using \<open>subseq r0\<close> by (simp add: seq_suble)
1.57 +    have "(1/2::real)^(r0 n) \<le> (1/2)^n" by (rule power_decreasing[OF \<open>r0 n \<ge> n\<close>], auto)
1.58      then have "(\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^n" using r0(2) less_le_trans by auto
1.59      then have "(\<integral>x. norm(u (r n) x) \<partial>M) < (1/2)^n" unfolding r_def by auto
1.60      moreover have "(\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M) = (\<integral>x. norm(u (r n) x) \<partial>M)"
1.61 @@ -2168,13 +2168,13 @@
1.62        also have "... \<le> (\<integral>\<^sup>+x. (1/e) * ennreal(norm(u (r n) x)) \<partial>M)"
1.63          apply (rule nn_integral_mono) using * by auto
1.64        also have "... = (1/e) * (\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M)"
1.65 -        apply (rule nn_integral_cmult) using e > 0 by auto
1.66 +        apply (rule nn_integral_cmult) using \<open>e > 0\<close> by auto
1.67        also have "... < (1/e) * ennreal((1/2)^n)"
1.68 -        using I[of n] e > 0 by (intro ennreal_mult_strict_left_mono) auto
1.69 +        using I[of n] \<open>e > 0\<close> by (intro ennreal_mult_strict_left_mono) auto
1.70        finally show ?thesis by simp
1.71      qed
1.72      have A_fin: "emeasure M (A n) < \<infinity>" for n
1.73 -      using e > 0 A_bound[of n]
1.74 +      using \<open>e > 0\<close> A_bound[of n]
1.75        by (auto simp add: ennreal_mult less_top[symmetric])
1.76
1.77      have A_sum: "summable (\<lambda>n. measure M (A n))"
1.78 @@ -2219,7 +2219,7 @@
1.79        by (simp add: tendsto_norm_zero_iff)
1.80    }
1.81    ultimately have "AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0" by auto
1.82 -  then show ?thesis using subseq r by auto
1.83 +  then show ?thesis using \<open>subseq r\<close> by auto
1.84  qed
1.85
1.86  subsection \<open>Restricted measure spaces\<close>

     2.1 --- a/src/HOL/Analysis/Borel_Space.thy	Tue Jan 17 11:26:21 2017 +0100
2.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Tue Jan 17 13:59:10 2017 +0100
2.3 @@ -2126,7 +2126,7 @@
2.4    shows "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> borel_measurable M"
2.5  unfolding powr_def by auto
2.6
2.7 -text {* The next one is a variation around \verb+measurable_restrict_space+.*}
2.8 +text \<open>The next one is a variation around \verb+measurable_restrict_space+.\<close>
2.9
2.10  lemma measurable_restrict_space3:
2.11    assumes "f \<in> measurable M N" and
2.12 @@ -2138,7 +2138,7 @@
2.13        measurable_restrict_space2[of f, of "restrict_space M A", of B, of N] assms(2) space_restrict_space)
2.14  qed
2.15
2.16 -text {* The next one is a variation around \verb+measurable_piecewise_restrict+.*}
2.17 +text \<open>The next one is a variation around \verb+measurable_piecewise_restrict+.\<close>
2.18
2.19  lemma measurable_piecewise_restrict2:
2.20    assumes [measurable]: "\<And>n. A n \<in> sets M"
2.21 @@ -2162,8 +2162,8 @@
2.22    fix x assume "x \<in> space M"
2.23    then obtain n where "x \<in> A n" using assms(2) by blast
2.24    obtain h where [measurable]: "h \<in> measurable M N" and "\<forall>x \<in> A n. f x = h x" using assms(3) by blast
2.25 -  then have "f x = h x" using x \<in> A n by blast
2.26 -  moreover have "h x \<in> space N" by (metis measurable_space x \<in> space M h \<in> measurable M N)
2.27 +  then have "f x = h x" using \<open>x \<in> A n\<close> by blast
2.28 +  moreover have "h x \<in> space N" by (metis measurable_space \<open>x \<in> space M\<close> \<open>h \<in> measurable M N\<close>)
2.29    ultimately show "f x \<in> space N" by simp
2.30  qed
2.31

     3.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Jan 17 11:26:21 2017 +0100
3.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Tue Jan 17 13:59:10 2017 +0100
3.3 @@ -2572,7 +2572,7 @@
3.4          moreover have False if "1 < dd (x - a)"
3.5            using x that dd2 [of "x - a" 1] \<open>x \<noteq> a\<close> closure_affine_hull
3.6            by (auto simp: rel_frontier_def)
3.7 -        ultimately have "dd (x - a) = 1" --\<open>similar to another proof above\<close>
3.8 +        ultimately have "dd (x - a) = 1" \<comment>\<open>similar to another proof above\<close>
3.9            by fastforce
3.10          with that show ?thesis
3.11            by (simp add: rel_frontier_def)

     4.1 --- a/src/HOL/Analysis/Function_Topology.thy	Tue Jan 17 11:26:21 2017 +0100
4.2 +++ b/src/HOL/Analysis/Function_Topology.thy	Tue Jan 17 13:59:10 2017 +0100
4.3 @@ -7,9 +7,9 @@
4.4  begin
4.5
4.6
4.7 -section {*Product topology*}
4.8 +section \<open>Product topology\<close>
4.9
4.10 -text {*We want to define the product topology.
4.11 +text \<open>We want to define the product topology.
4.12
4.13  The product topology on a product of topological spaces is generated by
4.14  the sets which are products of open sets along finitely many coordinates, and the whole
4.15 @@ -60,18 +60,18 @@
4.16  topology, even when the product is not finite (or even countable).
4.17
4.18  I realized afterwards that this theory has a lot in common with \verb+Fin_Map.thy+.
4.19 -*}
4.20 +\<close>
4.21
4.22 -subsection {*Topology without type classes*}
4.23 +subsection \<open>Topology without type classes\<close>
4.24
4.25 -subsubsection {*The topology generated by some (open) subsets*}
4.26 +subsubsection \<open>The topology generated by some (open) subsets\<close>
4.27
4.28 -text {* In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
4.29 +text \<open>In the definition below of a generated topology, the \<open>Empty\<close> case is not necessary,
4.30  as it follows from \<open>UN\<close> taking for $K$ the empty set. However, it is convenient to have,
4.31  and is never a problem in proofs, so I prefer to write it down explicitly.
4.32
4.33  We do not require UNIV to be an open set, as this will not be the case in applications. (We are
4.34 -thinking of a topology on a subset of UNIV, the remaining part of UNIV being irrelevant.)*}
4.35 +thinking of a topology on a subset of UNIV, the remaining part of UNIV being irrelevant.)\<close>
4.36
4.37  inductive generate_topology_on for S where
4.38  Empty: "generate_topology_on S {}"
4.39 @@ -83,8 +83,8 @@
4.40    "istopology (generate_topology_on S)"
4.41  unfolding istopology_def by (auto intro: generate_topology_on.intros)
4.42
4.43 -text {*The basic property of the topology generated by a set $S$ is that it is the
4.44 -smallest topology containing all the elements of $S$:*}
4.45 +text \<open>The basic property of the topology generated by a set $S$ is that it is the
4.46 +smallest topology containing all the elements of $S$:\<close>
4.47
4.48  lemma generate_topology_on_coarsest:
4.49    assumes "istopology T"
4.50 @@ -127,10 +127,10 @@
4.51    "s \<in> S \<Longrightarrow> openin (topology_generated_by S) s"
4.52  by (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis)
4.53
4.54 -subsubsection {*Continuity*}
4.55 +subsubsection \<open>Continuity\<close>
4.56
4.57 -text {*We will need to deal with continuous maps in terms of topologies and not in terms
4.58 -of type classes, as defined below.*}
4.59 +text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
4.60 +of type classes, as defined below.\<close>
4.61
4.62  definition continuous_on_topo::"'a topology \<Rightarrow> 'b topology \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
4.63    where "continuous_on_topo T1 T2 f = ((\<forall> U. openin T2 U \<longrightarrow> openin T1 (f-U \<inter> topspace(T1)))
4.64 @@ -206,15 +206,15 @@
4.65  using assms unfolding continuous_on_topo_def by auto
4.66
4.67
4.68 -subsubsection {*Pullback topology*}
4.69 +subsubsection \<open>Pullback topology\<close>
4.70
4.71 -text {*Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
4.72 +text \<open>Pulling back a topology by map gives again a topology. \<open>subtopology\<close> is
4.73  a special case of this notion, pulling back by the identity. We introduce the general notion as
4.74  we will need it to define the strong operator topology on the space of continuous linear operators,
4.75 -by pulling back the product topology on the space of all functions.*}
4.76 +by pulling back the product topology on the space of all functions.\<close>
4.77
4.78 -text {*\verb+pullback_topology A f T+ is the pullback of the topology $T$ by the map $f$ on
4.79 -the set $A$.*}
4.80 +text \<open>\verb+pullback_topology A f T+ is the pullback of the topology $T$ by the map $f$ on
4.81 +the set $A$.\<close>
4.82
4.83  definition pullback_topology::"('a set) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b topology) \<Rightarrow> ('a topology)"
4.84    where "pullback_topology A f T = topology (\<lambda>S. \<exists>U. openin T U \<and> S = f-U \<inter> A)"
4.85 @@ -253,7 +253,7 @@
4.86    also have "... = f-(g-U \<inter> topspace T1) \<inter> A "
4.87      by auto
4.88    also have "openin (pullback_topology A f T1) (...)"
4.89 -    unfolding openin_pullback_topology using openin T1 (g-\U \<inter> topspace T1) by auto
4.90 +    unfolding openin_pullback_topology using \<open>openin T1 (g-U \<inter> topspace T1)\<close> by auto
4.91    finally show "openin (pullback_topology A f T1) ((g \<circ> f) - U \<inter> topspace (pullback_topology A f T1))"
4.92      by auto
4.93  next
4.94 @@ -281,23 +281,23 @@
4.95    also have "... = (f o g)-V \<inter> topspace T1"
4.96      using assms(2) by auto
4.97    also have "openin T1 (...)"
4.98 -    using assms(1) openin T2 V by auto
4.99 +    using assms(1) \<open>openin T2 V\<close> by auto
4.100    finally show "openin T1 (g - U \<inter> topspace T1)" by simp
4.101  next
4.102    fix x assume "x \<in> topspace T1"
4.103    have "(f o g) x \<in> topspace T2"
4.104 -    using assms(1) x \<in> topspace T1 unfolding continuous_on_topo_def by auto
4.105 +    using assms(1) \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
4.106    then have "g x \<in> f-(topspace T2)"
4.107      unfolding comp_def by blast
4.108 -  moreover have "g x \<in> A" using assms(2) x \<in> topspace T1 by blast
4.109 +  moreover have "g x \<in> A" using assms(2) \<open>x \<in> topspace T1\<close> by blast
4.110    ultimately show "g x \<in> topspace (pullback_topology A f T2)"
4.111      unfolding topspace_pullback_topology by blast
4.112  qed
4.113
4.114
4.115 -subsection {*The product topology*}
4.116 +subsection \<open>The product topology\<close>
4.117
4.118 -text {*We can now define the product topology, as generated by
4.119 +text \<open>We can now define the product topology, as generated by
4.120  the sets which are products of open sets along finitely many coordinates, and the whole
4.121  space along the other coordinates. Equivalently, it is generated by sets which are one open
4.122  set along one single coordinate, and the whole space along other coordinates. In fact, this is only
4.123 @@ -306,14 +306,14 @@
4.124  point, equal to \verb+undefined+ along all coordinates.
4.125
4.126  So, we use the first formulation, which moreover seems to give rise to more straightforward proofs.
4.127 -*}
4.128 +\<close>
4.129
4.130  definition product_topology::"('i \<Rightarrow> ('a topology)) \<Rightarrow> ('i set) \<Rightarrow> (('i \<Rightarrow> 'a) topology)"
4.131    where "product_topology T I =
4.132      topology_generated_by {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
4.133
4.134 -text {*The total set of the product topology is the product of the total sets
4.135 -along each coordinate.*}
4.136 +text \<open>The total set of the product topology is the product of the total sets
4.137 +along each coordinate.\<close>
4.138
4.139  lemma product_topology_topspace:
4.140    "topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"
4.141 @@ -367,15 +367,15 @@
4.142      then obtain X where "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> k"
4.143        by blast
4.144      then have "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> (\<Union>K)"
4.145 -      using k \<in> K by auto
4.146 +      using \<open>k \<in> K\<close> by auto
4.147      then show ?case
4.148        by auto
4.149    qed auto
4.150 -  then show ?thesis using x \<in> U by auto
4.151 +  then show ?thesis using \<open>x \<in> U\<close> by auto
4.152  qed
4.153
4.154
4.155 -text {*The basic property of the product topology is the continuity of projections:*}
4.156 +text \<open>The basic property of the product topology is the continuity of projections:\<close>
4.157
4.158  lemma continuous_on_topo_product_coordinates [simp]:
4.159    assumes "i \<in> I"
4.160 @@ -385,10 +385,10 @@
4.161      fix U assume "openin (T i) U"
4.162      define X where "X = (\<lambda>j. if j = i then U else topspace (T j))"
4.163      then have *: "(\<lambda>x. x i) - U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)) = (\<Pi>\<^sub>E j\<in>I. X j)"
4.164 -      unfolding X_def using assms openin_subset[OF openin (T i) U]
4.165 +      unfolding X_def using assms openin_subset[OF \<open>openin (T i) U\<close>]
4.166        by (auto simp add: PiE_iff, auto, metis subsetCE)
4.167      have **: "(\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}"
4.168 -      unfolding X_def using openin (T i) U by auto
4.169 +      unfolding X_def using \<open>openin (T i) U\<close> by auto
4.170      have "openin (product_topology T I) ((\<lambda>x. x i) - U \<inter> (\<Pi>\<^sub>E i\<in>I. topspace (T i)))"
4.171        unfolding product_topology_def
4.172        apply (rule topology_generated_by_Basis)
4.173 @@ -417,11 +417,11 @@
4.174    have "f-U \<inter> topspace T1 = (\<Inter>i\<in>I. (\<lambda>x. f x i)-(X i) \<inter> topspace T1) \<inter> (topspace T1)"
4.175      by (subst H(1), auto simp add: PiE_iff assms)
4.176    also have "... = (\<Inter>i\<in>J. (\<lambda>x. f x i)-(X i) \<inter> topspace T1) \<inter> (topspace T1)"
4.177 -    using * J \<subseteq> I by auto
4.178 +    using * \<open>J \<subseteq> I\<close> by auto
4.179    also have "openin T1 (...)"
4.180      apply (rule openin_INT)
4.181 -    apply (simp add: finite J)
4.182 -    using H(2) assms(1) J \<subseteq> I by auto
4.183 +    apply (simp add: \<open>finite J\<close>)
4.184 +    using H(2) assms(1) \<open>J \<subseteq> I\<close> by auto
4.185    ultimately show "openin T1 (f-U \<inter> topspace T1)" by simp
4.186  next
4.187    show "f topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
4.188 @@ -441,17 +441,17 @@
4.189    have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f" by auto
4.190    also have "continuous_on_topo T1 (T i) (...)"
4.191      apply (rule continuous_on_topo_compose[of _ "product_topology T I"])
4.192 -    using assms i \<in> I by auto
4.193 +    using assms \<open>i \<in> I\<close> by auto
4.194    ultimately show "continuous_on_topo T1 (T i) (\<lambda>x. f x i)"
4.195      by simp
4.196  next
4.197    fix i x assume "i \<notin> I" "x \<in> topspace T1"
4.198    have "f x \<in> topspace (product_topology T I)"
4.199 -    using assms x \<in> topspace T1 unfolding continuous_on_topo_def by auto
4.200 +    using assms \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
4.201    then have "f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
4.202      using product_topology_topspace by metis
4.203    then show "f x i = undefined"
4.204 -    using i \<notin> I by (auto simp add: PiE_iff extensional_def)
4.205 +    using \<open>i \<notin> I\<close> by (auto simp add: PiE_iff extensional_def)
4.206  qed
4.207
4.208  lemma continuous_on_restrict:
4.209 @@ -461,7 +461,7 @@
4.210    fix i assume "i \<in> J"
4.211    then have "(\<lambda>x. restrict x J i) = (\<lambda>x. x i)" unfolding restrict_def by auto
4.212    then show "continuous_on_topo (product_topology T I) (T i) (\<lambda>x. restrict x J i)"
4.213 -    using i \<in> J J \<subseteq> I by auto
4.214 +    using \<open>i \<in> J\<close> \<open>J \<subseteq> I\<close> by auto
4.215  next
4.216    fix i assume "i \<notin> J"
4.217    then show "restrict x J i = undefined" for x::"'a \<Rightarrow> 'b"
4.218 @@ -469,7 +469,7 @@
4.219  qed
4.220
4.221
4.222 -subsubsection {*Powers of a single topological space as a topological space, using type classes*}
4.223 +subsubsection \<open>Powers of a single topological space as a topological space, using type classes\<close>
4.224
4.225  instantiation "fun" :: (type, topological_space) topological_space
4.226  begin
4.227 @@ -521,8 +521,8 @@
4.228    ultimately show ?thesis by simp
4.229  qed
4.230
4.231 -text {*The results proved in the general situation of products of possibly different
4.232 -spaces have their counterparts in this simpler setting.*}
4.233 +text \<open>The results proved in the general situation of products of possibly different
4.234 +spaces have their counterparts in this simpler setting.\<close>
4.235
4.236  lemma continuous_on_product_coordinates [simp]:
4.237    "continuous_on UNIV (\<lambda>x. x i::('b::topological_space))"
4.238 @@ -545,11 +545,11 @@
4.239    "continuous_on UNIV f \<longleftrightarrow> (\<forall>i. continuous_on UNIV (\<lambda>x. f x i))"
4.240  by (auto intro: continuous_on_product_then_coordinatewise)
4.241
4.242 -subsubsection {*Topological countability for product spaces*}
4.243 +subsubsection \<open>Topological countability for product spaces\<close>
4.244
4.245 -text {*The next two lemmas are useful to prove first or second countability
4.246 +text \<open>The next two lemmas are useful to prove first or second countability
4.247  of product spaces, but they have more to do with countability and could
4.248 -be put in the corresponding theory.*}
4.249 +be put in the corresponding theory.\<close>
4.250
4.251  lemma countable_nat_product_event_const:
4.252    fixes F::"'a set" and a::'a
4.253 @@ -563,7 +563,7 @@
4.254    proof (induction N)
4.255      case 0
4.256      have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>(0::nat). x i = a)} = {(\<lambda>i. a)}"
4.257 -      using a \<in> F by auto
4.258 +      using \<open>a \<in> F\<close> by auto
4.259      then show ?case by auto
4.260    next
4.261      case (Suc N)
4.262 @@ -576,7 +576,7 @@
4.263        have "f (y, x N) = x"
4.264          unfolding f_def y_def by auto
4.265        moreover have "(y, x N) \<in> {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F"
4.266 -        unfolding y_def using H a \<in> F by auto
4.267 +        unfolding y_def using H \<open>a \<in> F\<close> by auto
4.268        ultimately show "x \<in> f({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
4.269          by (metis (no_types, lifting) image_eqI)
4.270      qed
4.271 @@ -616,7 +616,7 @@
4.272        by auto
4.273    qed
4.274    then show ?thesis
4.275 -    using countable_nat_product_event_const[OF b \<in> G countable G]
4.276 +    using countable_nat_product_event_const[OF \<open>b \<in> G\<close> \<open>countable G\<close>]
4.277      by (meson countable_image countable_subset)
4.278  qed
4.279
4.280 @@ -629,7 +629,7 @@
4.281                                                    "\<And>x i. open (A x i)"
4.282                                                    "\<And>x S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>i. A x i \<subseteq> S)"
4.283      by metis
4.284 -  text {*$B i$ is a countable basis of neighborhoods of $x_i$.*}
4.285 +  text \<open>$B i$ is a countable basis of neighborhoods of $x_i$.\<close>
4.286    define B where "B = (\<lambda>i. (A (x i))UNIV \<union> {UNIV})"
4.287    have "countable (B i)" for i unfolding B_def by auto
4.288
4.289 @@ -638,7 +638,7 @@
4.290      unfolding K_def B_def by auto
4.291    then have "K \<noteq> {}" by auto
4.292    have "countable {X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
4.293 -    apply (rule countable_product_event_const) using \<And>i. countable (B i) by auto
4.294 +    apply (rule countable_product_event_const) using \<open>\<And>i. countable (B i)\<close> by auto
4.295    moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X){X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
4.296      unfolding K_def by auto
4.297    ultimately have "countable K" by auto
4.298 @@ -652,7 +652,7 @@
4.299    have Inc: "\<exists>k\<in>K. k \<subseteq> U" if "open U \<and> x \<in> U" for U
4.300    proof -
4.301      have "openin (product_topology (\<lambda>i. euclidean) UNIV) U" "x \<in> U"
4.302 -      using open U \<and> x \<in> U unfolding open_fun_def by auto
4.303 +      using \<open>open U \<and> x \<in> U\<close> unfolding open_fun_def by auto
4.304      with product_topology_open_contains_basis[OF this]
4.305      have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
4.306        unfolding topspace_euclidean open_openin by simp
4.307 @@ -685,12 +685,12 @@
4.308        apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
4.309      then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
4.310      then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
4.311 -    then show ?thesis using Pi\<^sub>E UNIV Y \<in> K by auto
4.312 +    then show ?thesis using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> by auto
4.313    qed
4.314
4.315    show "\<exists>L. (\<forall>(i::nat). x \<in> L i \<and> open (L i)) \<and> (\<forall>U. open U \<and> x \<in> U \<longrightarrow> (\<exists>i. L i \<subseteq> U))"
4.316      apply (rule first_countableI[of K])
4.317 -    using countable K \<And>k. k \<in> K \<Longrightarrow> x \<in> k \<And>k. k \<in> K \<Longrightarrow> open k Inc by auto
4.318 +    using \<open>countable K\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> x \<in> k\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> open k\<close> Inc by auto
4.319  qed
4.320
4.321  lemma product_topology_countable_basis:
4.322 @@ -709,10 +709,10 @@
4.323
4.324    define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i::'a. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
4.325    have i: "\<forall>k\<in>K. \<exists>X. (k = Pi\<^sub>E UNIV X) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV}"
4.326 -    unfolding K_def using \<And>U. U \<in> B2 \<Longrightarrow> open U by auto
4.327 +    unfolding K_def using \<open>\<And>U. U \<in> B2 \<Longrightarrow> open U\<close> by auto
4.328
4.329    have "countable {X. (\<forall>(i::'a). X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
4.330 -    apply (rule countable_product_event_const) using countable B2 by auto
4.331 +    apply (rule countable_product_event_const) using \<open>countable B2\<close> by auto
4.332    moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X){X. (\<forall>i. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
4.333      unfolding K_def by auto
4.334    ultimately have ii: "countable K" by auto
4.335 @@ -722,7 +722,7 @@
4.336      fix U and x::"'a\<Rightarrow>'b" assume "open U" "x \<in> U"
4.337      then have "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
4.338        unfolding open_fun_def by auto
4.339 -    with product_topology_open_contains_basis[OF this x \<in> U]
4.340 +    with product_topology_open_contains_basis[OF this \<open>x \<in> U\<close>]
4.341      have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
4.342        unfolding topspace_euclidean open_openin by simp
4.343      then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
4.344 @@ -734,7 +734,7 @@
4.345      define I where "I = {i. X i \<noteq> UNIV}"
4.346      define Y where "Y = (\<lambda>i. if i \<in> I then (SOME y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y) else UNIV)"
4.347      have *: "\<exists>y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y" for i
4.348 -      unfolding B2_def using B open (X i) x i \<in> X i by (meson UnCI topological_basisE)
4.349 +      unfolding B2_def using B \<open>open (X i)\<close> \<open>x i \<in> X i\<close> by (meson UnCI topological_basisE)
4.350      have **: "Y i \<in> B2 \<and> Y i \<subseteq> X i \<and> x i \<in> Y i" for i
4.351        using someI_ex[OF *]
4.352        apply (cases "i \<in> I")
4.353 @@ -758,13 +758,13 @@
4.354        using ** by auto
4.355
4.356      show "\<exists>V\<in>K. x \<in> V \<and> V \<subseteq> U"
4.357 -      using Pi\<^sub>E UNIV Y \<in> K Pi\<^sub>E UNIV Y \<subseteq> U x \<in> Pi\<^sub>E UNIV Y by auto
4.358 +      using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> \<open>Pi\<^sub>E UNIV Y \<subseteq> U\<close> \<open>x \<in> Pi\<^sub>E UNIV Y\<close> by auto
4.359    next
4.360      fix U assume "U \<in> K"
4.361      show "open U"
4.362 -      using U \<in> K unfolding open_fun_def K_def apply (auto)
4.363 +      using \<open>U \<in> K\<close> unfolding open_fun_def K_def apply (auto)
4.364        apply (rule product_topology_basis)
4.365 -      using \<And>V. V \<in> B2 \<Longrightarrow> open V open_UNIV unfolding topspace_euclidean open_openin[symmetric]
4.366 +      using \<open>\<And>V. V \<in> B2 \<Longrightarrow> open V\<close> open_UNIV unfolding topspace_euclidean open_openin[symmetric]
4.367        by auto
4.368    qed
4.369
4.370 @@ -776,9 +776,9 @@
4.371    using product_topology_countable_basis topological_basis_imp_subbasis by auto
4.372
4.373
4.374 -subsection {*The strong operator topology on continuous linear operators*}
4.375 +subsection \<open>The strong operator topology on continuous linear operators\<close>
4.376
4.377 -text {*Let 'a and 'b be two normed real vector spaces. Then the space of linear continuous
4.378 +text \<open>Let 'a and 'b be two normed real vector spaces. Then the space of linear continuous
4.379  operators from 'a to 'b has a canonical norm, and therefore a canonical corresponding topology
4.380  (the type classes instantiation are given in \verb+Bounded_Linear_Function.thy+).
4.381
4.382 @@ -795,7 +795,7 @@
4.383  weak-* topology, i.e., the pullback of the weak topology on the bidual of the space under the
4.384  canonical embedding of a space into its bidual. We do not define it there, although it could also be
4.385  defined analogously.
4.386 -*}
4.387 +\<close>
4.388
4.389  definition strong_operator_topology::"('a::real_normed_vector \<Rightarrow>\<^sub>L'b::real_normed_vector) topology"
4.390  where "strong_operator_topology = pullback_topology UNIV blinfun_apply euclidean"
4.391 @@ -847,7 +847,7 @@
4.392    show "continuous_on_topo T strong_operator_topology f"
4.393      unfolding strong_operator_topology_def
4.394      apply (rule continuous_on_topo_pullback')
4.395 -    by (auto simp add: continuous_on_topo T euclidean (blinfun_apply o f))
4.396 +    by (auto simp add: \<open>continuous_on_topo T euclidean (blinfun_apply o f)\<close>)
4.397  qed
4.398
4.399  lemma strong_operator_topology_weaker_than_euclidean:
4.400 @@ -856,10 +856,10 @@
4.401      auto simp add: continuous_on_topo_UNIV[symmetric] linear_continuous_on)
4.402
4.403
4.404 -subsection {*Metrics on product spaces*}
4.405 +subsection \<open>Metrics on product spaces\<close>
4.406
4.407
4.408 -text {*In general, the product topology is not metrizable, unless the index set is countable.
4.409 +text \<open>In general, the product topology is not metrizable, unless the index set is countable.
4.410  When the index set is countable, essentially any (convergent) combination of the metrics on the
4.411  factors will do. We use below the simplest one, based on $L^1$, but $L^2$ would also work,
4.412  for instance.
4.413 @@ -870,7 +870,7 @@
4.414
4.415  The proofs below would work verbatim for general countable products of metric spaces. However,
4.416  since distances are only implemented in terms of type classes, we only develop the theory
4.417 -for countable products of the same space.*}
4.418 +for countable products of the same space.\<close>
4.419
4.420  instantiation "fun" :: (countable, metric_space) metric_space
4.421  begin
4.422 @@ -881,10 +881,10 @@
4.423  definition uniformity_fun_def:
4.424    "(uniformity::(('a \<Rightarrow> 'b) \<times> ('a \<Rightarrow> 'b)) filter) = (INF e:{0<..}. principal {(x, y). dist (x::('a\<Rightarrow>'b)) y < e})"
4.425
4.426 -text {*Except for the first one, the auxiliary lemmas below are only useful when proving the
4.427 +text \<open>Except for the first one, the auxiliary lemmas below are only useful when proving the
4.428  instance: once it is proved, they become trivial consequences of the general theory of metric
4.429  spaces. It would thus be desirable to hide them once the instance is proved, but I do not know how
4.430 -to do this.*}
4.431 +to do this.\<close>
4.432
4.433  lemma dist_fun_le_dist_first_terms:
4.434    "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
4.435 @@ -947,18 +947,18 @@
4.436                      "\<And>i. openin euclidean (X i)"
4.437                      "finite {i. X i \<noteq> topspace euclidean}"
4.438                      "x \<in> Pi\<^sub>E UNIV X"
4.439 -    using product_topology_open_contains_basis[OF * x \<in> U] by auto
4.440 +    using product_topology_open_contains_basis[OF * \<open>x \<in> U\<close>] by auto
4.441    define I where "I = {i. X i \<noteq> topspace euclidean}"
4.442    have "finite I" unfolding I_def using H(3) by auto
4.443    {
4.444      fix i
4.445 -    have "x i \<in> X i" using x \<in> U H by auto
4.446 +    have "x i \<in> X i" using \<open>x \<in> U\<close> H by auto
4.447      then have "\<exists>e. e>0 \<and> ball (x i) e \<subseteq> X i"
4.448 -      using openin euclidean (X i) open_openin open_contains_ball by blast
4.449 +      using \<open>openin euclidean (X i)\<close> open_openin open_contains_ball by blast
4.450      then obtain e where "e>0" "ball (x i) e \<subseteq> X i" by blast
4.451      define f where "f = min e (1/2)"
4.452 -    have "f>0" "f<1" unfolding f_def using e>0 by auto
4.453 -    moreover have "ball (x i) f \<subseteq> X i" unfolding f_def using ball (x i) e \<subseteq> X i by auto
4.454 +    have "f>0" "f<1" unfolding f_def using \<open>e>0\<close> by auto
4.455 +    moreover have "ball (x i) f \<subseteq> X i" unfolding f_def using \<open>ball (x i) e \<subseteq> X i\<close> by auto
4.456      ultimately have "\<exists>f. f > 0 \<and> f < 1 \<and> ball (x i) f \<subseteq> X i" by auto
4.457    } note * = this
4.458    have "\<exists>e. \<forall>i. e i > 0 \<and> e i < 1 \<and> ball (x i) (e i) \<subseteq> X i"
4.459 @@ -967,7 +967,7 @@
4.460      by blast
4.461    define m where "m = Min {(1/2)^(to_nat i) * e i|i. i \<in> I}"
4.462    have "m > 0" if "I\<noteq>{}"
4.463 -    unfolding m_def apply (rule Min_grI) using finite I I \<noteq> {} \<And>i. e i > 0 by auto
4.464 +    unfolding m_def apply (rule Min_grI) using \<open>finite I\<close> \<open>I \<noteq> {}\<close> \<open>\<And>i. e i > 0\<close> by auto
4.465    moreover have "{y. dist x y < m} \<subseteq> U"
4.466    proof (auto)
4.467      fix y assume "dist x y < m"
4.468 @@ -977,19 +977,19 @@
4.469          by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
4.470        define n where "n = to_nat i"
4.471        have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 < m"
4.472 -        using dist x y < m unfolding dist_fun_def using sum_le_suminf[OF *, of "{n}"] by auto
4.473 +        using \<open>dist x y < m\<close> unfolding dist_fun_def using sum_le_suminf[OF *, of "{n}"] by auto
4.474        then have "(1/2)^(to_nat i) * min (dist (x i) (y i)) 1 < m"
4.475 -        using n = to_nat i by auto
4.476 +        using \<open>n = to_nat i\<close> by auto
4.477        also have "... \<le> (1/2)^(to_nat i) * e i"
4.478 -        unfolding m_def apply (rule Min_le) using finite I i \<in> I by auto
4.479 +        unfolding m_def apply (rule Min_le) using \<open>finite I\<close> \<open>i \<in> I\<close> by auto
4.480        ultimately have "min (dist (x i) (y i)) 1 < e i"
4.481          by (auto simp add: divide_simps)
4.482        then have "dist (x i) (y i) < e i"
4.483 -        using e i < 1 by auto
4.484 -      then show "y i \<in> X i" using ball (x i) (e i) \<subseteq> X i by auto
4.485 +        using \<open>e i < 1\<close> by auto
4.486 +      then show "y i \<in> X i" using \<open>ball (x i) (e i) \<subseteq> X i\<close> by auto
4.487      qed
4.488      then have "y \<in> Pi\<^sub>E UNIV X" using H(1) unfolding I_def topspace_euclidean by (auto simp add: PiE_iff)
4.489 -    then show "y \<in> U" using Pi\<^sub>E UNIV X \<subseteq> U by auto
4.490 +    then show "y \<in> U" using \<open>Pi\<^sub>E UNIV X \<subseteq> U\<close> by auto
4.491    qed
4.492    ultimately have *: "\<exists>m>0. {y. dist x y < m} \<subseteq> U" if "I \<noteq> {}" using that by auto
4.493
4.494 @@ -1021,14 +1021,14 @@
4.495    define U where "U = Pi\<^sub>E UNIV X"
4.496    have "open U"
4.497      unfolding open_fun_def product_topology_def apply (rule topology_generated_by_Basis)
4.498 -    unfolding U_def using \<And>i. openin euclidean (X i) finite {i. X i \<noteq> topspace euclidean}
4.499 +    unfolding U_def using \<open>\<And>i. openin euclidean (X i)\<close> \<open>finite {i. X i \<noteq> topspace euclidean}\<close>
4.500      by auto
4.501    moreover have "x \<in> U"
4.502      unfolding U_def X_def by (auto simp add: PiE_iff)
4.503    moreover have "dist x y < e" if "y \<in> U" for y
4.504    proof -
4.505      have *: "dist (x (from_nat n)) (y (from_nat n)) \<le> f" if "n \<le> N" for n
4.506 -      using y \<in> U unfolding U_def apply (auto simp add: PiE_iff)
4.507 +      using \<open>y \<in> U\<close> unfolding U_def apply (auto simp add: PiE_iff)
4.508        unfolding X_def using that by (metis less_imp_le mem_Collect_eq)
4.509      have **: "Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} \<le> f"
4.510        apply (rule Max.boundedI) using * by auto
4.511 @@ -1036,7 +1036,7 @@
4.512      have "dist x y \<le> 2 * Max {dist (x (from_nat n)) (y (from_nat n))|n. n \<le> N} + (1/2)^N"
4.513        by (rule dist_fun_le_dist_first_terms)
4.514      also have "... \<le> 2 * f + e / 8"
4.515 -      apply (rule add_mono) using ** 2^N > 8/e by(auto simp add: algebra_simps divide_simps)
4.516 +      apply (rule add_mono) using ** \<open>2^N > 8/e\<close> by(auto simp add: algebra_simps divide_simps)
4.517      also have "... \<le> e/2 + e/8"
4.518        unfolding f_def by auto
4.519      also have "... < e"
4.520 @@ -1053,7 +1053,7 @@
4.521    assume "open U"
4.522    fix x assume "x \<in> U"
4.523    then show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
4.524 -    using open_fun_contains_ball_aux[OF open U x \<in> U] by auto
4.525 +    using open_fun_contains_ball_aux[OF \<open>open U\<close> \<open>x \<in> U\<close>] by auto
4.526  next
4.527    assume H: "\<forall>x\<in>U. \<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> y \<in> U"
4.528    define K where "K = {V. open V \<and> V \<subseteq> U}"
4.529 @@ -1061,10 +1061,10 @@
4.530      fix x assume "x \<in> U"
4.531      then obtain e where e: "e>0" "{y. dist x y < e} \<subseteq> U" using H by blast
4.532      then obtain V where V: "open V" "x \<in> V" "V \<subseteq> {y. dist x y < e}"
4.533 -      using ball_fun_contains_open_aux[OF e>0, of x] by auto
4.534 +      using ball_fun_contains_open_aux[OF \<open>e>0\<close>, of x] by auto
4.535      have "V \<in> K"
4.536        unfolding K_def using e(2) V(1) V(3) by auto
4.537 -    then have "x \<in> (\<Union>K)" using x \<in> V by auto
4.538 +    then have "x \<in> (\<Union>K)" using \<open>x \<in> V\<close> by auto
4.539    }
4.540    then have "(\<Union>K) = U"
4.541      unfolding K_def by auto
4.542 @@ -1077,13 +1077,13 @@
4.543    fix x y::"'a \<Rightarrow> 'b" show "(dist x y = 0) = (x = y)"
4.544    proof
4.545      assume "x = y"
4.546 -    then show "dist x y = 0" unfolding dist_fun_def using x = y by auto
4.547 +    then show "dist x y = 0" unfolding dist_fun_def using \<open>x = y\<close> by auto
4.548    next
4.549      assume "dist x y = 0"
4.550      have *: "summable (\<lambda>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
4.551        by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
4.552      have "(1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1 = 0" for n
4.553 -      using dist x y = 0 unfolding dist_fun_def by (simp add: "*" suminf_eq_zero_iff)
4.554 +      using \<open>dist x y = 0\<close> unfolding dist_fun_def by (simp add: "*" suminf_eq_zero_iff)
4.555      then have "dist (x (from_nat n)) (y (from_nat n)) = 0" for n
4.556        by (metis div_0 min_def nonzero_mult_div_cancel_left power_eq_0_iff
4.557                  zero_eq_1_divide_iff zero_neq_numeral)
4.558 @@ -1095,9 +1095,9 @@
4.559        by auto
4.560    qed
4.561  next
4.562 -  text{*The proof of the triangular inequality is trivial, modulo the fact that we are dealing
4.563 +  text\<open>The proof of the triangular inequality is trivial, modulo the fact that we are dealing
4.564          with infinite series, hence we should justify the convergence at each step. In this
4.565 -        respect, the following simplification rule is extremely handy.*}
4.566 +        respect, the following simplification rule is extremely handy.\<close>
4.567    have [simp]: "summable (\<lambda>n. (1/2)^n * min (dist (u (from_nat n)) (v (from_nat n))) 1)" for u v::"'a \<Rightarrow> 'b"
4.568      by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
4.569    fix x y z::"'a \<Rightarrow> 'b"
4.570 @@ -1134,11 +1134,11 @@
4.571    finally show "dist x y \<le> dist x z + dist y z"
4.572      by simp
4.573  next
4.574 -  text{*Finally, we show that the topology generated by the distance and the product
4.575 +  text\<open>Finally, we show that the topology generated by the distance and the product
4.576          topology coincide. This is essentially contained in Lemma \verb+fun_open_ball_aux+,
4.577          except that the condition to prove is expressed with filters. To deal with this,
4.578          we copy some mumbo jumbo from Lemma \verb+eventually_uniformity_metric+ in
4.579 -        \verb+Real_Vector_Spaces.thy+*}
4.580 +        \verb+Real_Vector_Spaces.thy+\<close>
4.581    fix U::"('a \<Rightarrow> 'b) set"
4.582    have "eventually P uniformity \<longleftrightarrow> (\<exists>e>0. \<forall>x (y::('a \<Rightarrow> 'b)). dist x y < e \<longrightarrow> P (x, y))" for P
4.583    unfolding uniformity_fun_def apply (subst eventually_INF_base)
4.584 @@ -1149,9 +1149,9 @@
4.585
4.586  end
4.587
4.588 -text {*Nice properties of spaces are preserved under countable products. In addition
4.589 +text \<open>Nice properties of spaces are preserved under countable products. In addition
4.590  to first countability, second countability and metrizability, as we have seen above,
4.591 -completeness is also preserved, and therefore being Polish.*}
4.592 +completeness is also preserved, and therefore being Polish.\<close>
4.593
4.594  instance "fun" :: (countable, complete_space) complete_space
4.595  proof
4.596 @@ -1161,9 +1161,9 @@
4.597      fix e assume "e>(0::real)"
4.598      obtain k where "i = from_nat k"
4.599        using from_nat_to_nat[of i] by metis
4.600 -    have "(1/2)^k * min e 1 > 0" using e>0 by auto
4.601 +    have "(1/2)^k * min e 1 > 0" using \<open>e>0\<close> by auto
4.602      then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"
4.603 -      using Cauchy u unfolding cauchy_def by blast
4.604 +      using \<open>Cauchy u\<close> unfolding cauchy_def by blast
4.605      then obtain N::nat where C: "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m) (u n) < (1/2)^k * min e 1"
4.606        by blast
4.607      have "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (u m i) (u n i) < e"
4.608 @@ -1171,14 +1171,14 @@
4.609        fix m n::nat assume "m \<ge> N" "n \<ge> N"
4.610        have "(1/2)^k * min (dist (u m i) (u n i)) 1
4.611                = sum (\<lambda>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1) {k}"
4.612 -        using i = from_nat k by auto
4.613 +        using \<open>i = from_nat k\<close> by auto
4.614        also have "... \<le> (\<Sum>p. (1/2)^p * min (dist (u m (from_nat p)) (u n (from_nat p))) 1)"
4.615          apply (rule sum_le_suminf)
4.616          by (rule summable_comparison_test'[of "\<lambda>n. (1/2)^n"], auto simp add: summable_geometric_iff)
4.617        also have "... = dist (u m) (u n)"
4.618          unfolding dist_fun_def by auto
4.619        also have "... < (1/2)^k * min e 1"
4.620 -        using C m \<ge> N n \<ge> N by auto
4.621 +        using C \<open>m \<ge> N\<close> \<open>n \<ge> N\<close> by auto
4.622        finally have "min (dist (u m i) (u n i)) 1 < min e 1"
4.623          by (auto simp add: algebra_simps divide_simps)
4.624        then show "dist (u m i) (u n i) < e" by auto
4.625 @@ -1210,8 +1210,8 @@
4.626        have *: "dist (u k (from_nat n)) (x (from_nat n)) \<le> e / 4" if "n \<le> N" for n
4.627        proof -
4.628          have "K (from_nat n) \<le> L"
4.629 -          unfolding L_def apply (rule Max_ge) using n \<le> N by auto
4.630 -        then have "k \<ge> K (from_nat n)" using k \<ge> L by auto
4.631 +          unfolding L_def apply (rule Max_ge) using \<open>n \<le> N\<close> by auto
4.632 +        then have "k \<ge> K (from_nat n)" using \<open>k \<ge> L\<close> by auto
4.633          then show ?thesis using K less_imp_le by auto
4.634        qed
4.635        have **: "Max {dist (u k (from_nat n)) (x (from_nat n)) |n. n \<le> N} \<le> e/4"
4.636 @@ -1220,7 +1220,7 @@
4.637          using dist_fun_le_dist_first_terms by auto
4.638        also have "... \<le> 2 * e/4 + e/4"
4.639          apply (rule add_mono)
4.640 -        using ** 2^N > 4/e less_imp_le by (auto simp add: algebra_simps divide_simps)
4.641 +        using ** \<open>2^N > 4/e\<close> less_imp_le by (auto simp add: algebra_simps divide_simps)
4.642        also have "... < e" by auto
4.643        finally show ?thesis by simp
4.644      qed
4.645 @@ -1233,9 +1233,9 @@
4.646  by standard
4.647
4.648
4.649 -subsection {*Measurability*}
4.650 +subsection \<open>Measurability\<close>
4.651
4.652 -text {*There are two natural sigma-algebras on a product space: the borel sigma algebra,
4.653 +text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
4.654  generated by open sets in the product, and the product sigma algebra, countably generated by
4.655  products of measurable sets along finitely many coordinates. The second one is defined and studied
4.656  in \verb+Finite_Product_Measure.thy+.
4.657 @@ -1249,7 +1249,7 @@
4.658
4.659  In this paragraph, we develop basic measurability properties for the borel sigma algebra, and
4.660  compare it with the product sigma algebra as explained above.
4.661 -*}
4.662 +\<close>
4.663
4.664  lemma measurable_product_coordinates [measurable (raw)]:
4.665    "(\<lambda>x. x i) \<in> measurable borel borel"
4.666 @@ -1265,9 +1265,9 @@
4.667    then show ?thesis by simp
4.668  qed
4.669
4.670 -text {*To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
4.671 +text \<open>To compare the Borel sigma algebra with the product sigma algebra, we give a presentation
4.672  of the product sigma algebra that is more similar to the one we used above for the product
4.673 -topology.*}
4.674 +topology.\<close>
4.675
4.676  lemma sets_PiM_finite:
4.677    "sets (Pi\<^sub>M I M) = sigma_sets (\<Pi>\<^sub>E i\<in>I. space (M i))
4.678 @@ -1281,7 +1281,7 @@
4.679      have "finite J" "J \<subseteq> I" unfolding J_def using H by auto
4.680      define Y where "Y = (\<Pi>\<^sub>E j\<in>J. X j)"
4.681      have "prod_emb I M J Y \<in> sets (Pi\<^sub>M I M)"
4.682 -      unfolding Y_def apply (rule sets_PiM_I) using finite J J \<subseteq> I * by auto
4.683 +      unfolding Y_def apply (rule sets_PiM_I) using \<open>finite J\<close> \<open>J \<subseteq> I\<close> * by auto
4.684      moreover have "prod_emb I M J Y = (\<Pi>\<^sub>E i\<in>I. X i)"
4.685        unfolding prod_emb_def Y_def J_def using H sets.sets_into_space[OF *]
4.686        by (auto simp add: PiE_iff, blast)
4.687 @@ -1297,10 +1297,10 @@
4.688    proof -
4.689      define X where "X = (\<lambda>j. if j = i then A else space (M j))"
4.690      have "{f. (\<forall>i\<in>I. f i \<in> space (M i)) \<and> f \<in> extensional I \<and> f i \<in> A} = Pi\<^sub>E I X"
4.691 -      unfolding X_def using sets.sets_into_space[OF A \<in> sets (M i)] i \<in> I
4.692 +      unfolding X_def using sets.sets_into_space[OF \<open>A \<in> sets (M i)\<close>] \<open>i \<in> I\<close>
4.693        by (auto simp add: PiE_iff extensional_def, metis subsetCE, metis)
4.694      moreover have "X j \<in> sets (M j)" for j
4.695 -      unfolding X_def using A \<in> sets (M i) by auto
4.696 +      unfolding X_def using \<open>A \<in> sets (M i)\<close> by auto
4.697      moreover have "finite {j. X j \<noteq> space (M j)}"
4.698        unfolding X_def by simp
4.699      ultimately show ?thesis by auto
4.700 @@ -1322,7 +1322,7 @@
4.701      have "Pi\<^sub>E UNIV X = (\<Inter>i\<in>I. (\<lambda>x. x i)-(X i) \<inter> space borel) \<inter> space borel"
4.702        unfolding I_def by auto
4.703      also have "... \<in> sets borel"
4.704 -      using that finite I by measurable
4.705 +      using that \<open>finite I\<close> by measurable
4.706      finally show ?thesis by simp
4.707    qed
4.708    then have "{(\<Pi>\<^sub>E i\<in>UNIV. X i) |X::('a \<Rightarrow> 'b set). (\<forall>i. X i \<in> sets borel) \<and> finite {i. X i \<noteq> space borel}} \<subseteq> sets borel"
4.709 @@ -1340,17 +1340,17 @@
4.710    have *: "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> K" for k
4.711    proof -
4.712      obtain X where H: "k = Pi\<^sub>E UNIV X" "\<And>i. open (X i)" "finite {i. X i \<noteq> UNIV}"
4.713 -      using K(3)[OF k \<in> K] by blast
4.714 +      using K(3)[OF \<open>k \<in> K\<close>] by blast
4.715      show ?thesis unfolding H(1) sets_PiM_finite space_borel using borel_open[OF H(2)] H(3) by auto
4.716    qed
4.717    have **: "U \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "open U" for U::"('a \<Rightarrow> 'b) set"
4.718    proof -
4.719      obtain B where "B \<subseteq> K" "U = (\<Union>B)"
4.720 -      using open U topological_basis K by (metis topological_basis_def)
4.721 -    have "countable B" using B \<subseteq> K countable K countable_subset by blast
4.722 +      using \<open>open U\<close> \<open>topological_basis K\<close> by (metis topological_basis_def)
4.723 +    have "countable B" using \<open>B \<subseteq> K\<close> \<open>countable K\<close> countable_subset by blast
4.724      moreover have "k \<in> sets (Pi\<^sub>M UNIV (\<lambda>_. borel))" if "k \<in> B" for k
4.725 -      using B \<subseteq> K * that by auto
4.726 -    ultimately show ?thesis unfolding U = (\<Union>B) by auto
4.727 +      using \<open>B \<subseteq> K\<close> * that by auto
4.728 +    ultimately show ?thesis unfolding \<open>U = (\<Union>B)\<close> by auto
4.729    qed
4.730    have "sigma_sets UNIV (Collect open) \<subseteq> sets (Pi\<^sub>M UNIV (\<lambda>i::'a. (borel::('b measure))))"
4.731      apply (rule sets.sigma_sets_subset') using ** by auto

     5.1 --- a/src/HOL/Analysis/Further_Topology.thy	Tue Jan 17 11:26:21 2017 +0100
5.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Tue Jan 17 13:59:10 2017 +0100
5.3 @@ -4350,7 +4350,7 @@
5.4    qed
5.5  qed
5.6
5.7 -text\<open>The proof is a duplicate of that of @{text Borsukian_open_Un}.\<close>
5.8 +text\<open>The proof is a duplicate of that of \<open>Borsukian_open_Un\<close>.\<close>
5.9  lemma Borsukian_closed_Un:
5.10    fixes S :: "'a::real_normed_vector set"
5.11    assumes cloS: "closedin (subtopology euclidean (S \<union> T)) S"

     6.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Jan 17 11:26:21 2017 +0100
6.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Jan 17 13:59:10 2017 +0100
6.3 @@ -109,7 +109,7 @@
6.4    fixes a :: "'a::euclidean_space"
6.5    assumes "k \<in> Basis"
6.6    shows "content (cbox a b) = content(cbox a b \<inter> {x. x\<bullet>k \<le> c}) + content(cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
6.7 -  -- \<open>Prove using measure theory\<close>
6.8 +  \<comment> \<open>Prove using measure theory\<close>
6.9  proof cases
6.10    note simps = interval_split[OF assms] content_cbox_cases
6.11    have *: "Basis = insert k (Basis - {k})" "\<And>x. finite (Basis-{x})" "\<And>x. x\<notin>Basis-{x}"

     7.1 --- a/src/HOL/Analysis/Measure_Space.thy	Tue Jan 17 11:26:21 2017 +0100
7.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Tue Jan 17 13:59:10 2017 +0100
7.3 @@ -1092,9 +1092,9 @@
7.4    qed
7.5  qed
7.6
7.7 -text {*The next lemma is convenient to combine with a lemma whose conclusion is of the
7.8 +text \<open>The next lemma is convenient to combine with a lemma whose conclusion is of the
7.9  form \<open>AE x in M. P x = Q x\<close>: for such a lemma, there is no \verb+[symmetric]+ variant,
7.10 -but using \<open>AE_symmetric[OF...]\<close> will replace it.*}
7.11 +but using \<open>AE_symmetric[OF...]\<close> will replace it.\<close>
7.12
7.13  (* depricated replace by laws about eventually *)
7.14  lemma
7.15 @@ -1361,19 +1361,19 @@
7.16      where A: "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>" "incseq A"
7.17      using sigma_finite_incseq by blast
7.18    define B where "B = (\<lambda>i. W \<inter> A i)"
7.19 -  have B_meas: "\<And>i. B i \<in> sets M" using W_meas range A \<subseteq> sets M B_def by blast
7.20 +  have B_meas: "\<And>i. B i \<in> sets M" using W_meas \<open>range A \<subseteq> sets M\<close> B_def by blast
7.21    have b: "\<And>i. B i \<subseteq> W" using B_def by blast
7.22
7.23    { fix i
7.24      have "emeasure M (B i) \<le> emeasure M (A i)"
7.25        using A by (intro emeasure_mono) (auto simp: B_def)
7.26      also have "emeasure M (A i) < \<infinity>"
7.27 -      using \<And>i. emeasure M (A i) \<noteq> \<infinity> by (simp add: less_top)
7.28 +      using \<open>\<And>i. emeasure M (A i) \<noteq> \<infinity>\<close> by (simp add: less_top)
7.29      finally have "emeasure M (B i) < \<infinity>" . }
7.30    note c = this
7.31
7.32 -  have "W = (\<Union>i. B i)" using B_def (\<Union>i. A i) = space M W_meas by auto
7.33 -  moreover have "incseq B" using B_def incseq A by (simp add: incseq_def subset_eq)
7.34 +  have "W = (\<Union>i. B i)" using B_def \<open>(\<Union>i. A i) = space M\<close> W_meas by auto
7.35 +  moreover have "incseq B" using B_def \<open>incseq A\<close> by (simp add: incseq_def subset_eq)
7.36    ultimately have "(\<lambda>i. emeasure M (B i)) \<longlonglongrightarrow> emeasure M W" using W_meas B_meas
7.37      by (simp add: B_meas Lim_emeasure_incseq image_subset_iff)
7.38    then have "(\<lambda>i. emeasure M (B i)) \<longlonglongrightarrow> \<infinity>" using W_inf by simp

     8.1 --- a/src/HOL/Analysis/Path_Connected.thy	Tue Jan 17 11:26:21 2017 +0100
8.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Tue Jan 17 13:59:10 2017 +0100
8.3 @@ -7099,7 +7099,7 @@
8.4
8.5  subsection\<open> Self-homeomorphisms shuffling points about in various ways.\<close>
8.6
8.7 -subsubsection\<open>The theorem @{text homeomorphism_moving_points_exists}\<close>
8.8 +subsubsection\<open>The theorem \<open>homeomorphism_moving_points_exists\<close>\<close>
8.9
8.10  lemma homeomorphism_moving_point_1:
8.11    fixes a :: "'a::euclidean_space"
8.12 @@ -7521,7 +7521,7 @@
8.13  qed
8.14
8.15
8.16 -subsubsection\<open>The theorem @{text homeomorphism_grouping_points_exists}\<close>
8.17 +subsubsection\<open>The theorem \<open>homeomorphism_grouping_points_exists\<close>\<close>
8.18
8.19  lemma homeomorphism_grouping_point_1:
8.20    fixes a::real and c::real

     9.1 --- a/src/HOL/Analysis/Radon_Nikodym.thy	Tue Jan 17 11:26:21 2017 +0100
9.2 +++ b/src/HOL/Analysis/Radon_Nikodym.thy	Tue Jan 17 13:59:10 2017 +0100
9.3 @@ -44,9 +44,9 @@
9.4    qed
9.5  qed fact
9.6
9.7 -text {*An equivalent characterization of sigma-finite spaces is the existence of integrable
9.8 +text \<open>An equivalent characterization of sigma-finite spaces is the existence of integrable
9.9  positive functions (or, still equivalently, the existence of a probability measure which is in
9.10 -the same measure class as the original measure).*}
9.11 +the same measure class as the original measure).\<close>
9.12
9.13  lemma (in sigma_finite_measure) obtain_positive_integrable_function:
9.14    obtains f::"'a \<Rightarrow> real" where
9.15 @@ -69,7 +69,7 @@
9.16
9.17    have g_pos: "g x > 0" if "x \<in> space M" for x
9.18    unfolding g_def proof (subst suminf_pos_iff[OF *[of x]], auto)
9.19 -    obtain i where "x \<in> A i" using (\<Union>i. A i) = space M x \<in> space M by auto
9.20 +    obtain i where "x \<in> A i" using \<open>(\<Union>i. A i) = space M\<close> \<open>x \<in> space M\<close> by auto
9.21      then have "0 < (1 / 2) ^ Suc i * indicator (A i) x / (1 + Sigma_Algebra.measure M (A i))"
9.22        unfolding indicator_def apply (auto simp add: divide_simps) using measure_nonneg[of M "A i"]
9.23        by (auto, meson add_nonneg_nonneg linorder_not_le mult_nonneg_nonneg zero_le_numeral zero_le_one zero_le_power)
9.24 @@ -81,7 +81,7 @@
9.25    unfolding g_def proof (rule integrable_suminf)
9.26      fix n
9.27      show "integrable M (\<lambda>x. (1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n)))"
9.28 -      using emeasure M (A n) \<noteq> \<infinity>
9.29 +      using \<open>emeasure M (A n) \<noteq> \<infinity>\<close>
9.30        by (auto intro!: integrable_mult_right integrable_divide_zero integrable_real_indicator simp add: top.not_eq_extremum)
9.31    next
9.32      show "AE x in M. summable (\<lambda>n. norm ((1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n))))"
9.33 @@ -97,7 +97,7 @@
9.34    moreover have "f x \<le> 1" for x unfolding f_def using g_le_1 by auto
9.35    moreover have [measurable]: "f \<in> borel_measurable M" unfolding f_def by auto
9.36    moreover have "integrable M f"
9.37 -    apply (subst integrable_cong[of _ _ _ g]) unfolding f_def using integrable M g by auto
9.38 +    apply (subst integrable_cong[of _ _ _ g]) unfolding f_def using \<open>integrable M g\<close> by auto
9.39    ultimately show "(\<And>f. f \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 < f x) \<Longrightarrow> (\<And>x. f x \<le> 1) \<Longrightarrow> integrable M f \<Longrightarrow> thesis) \<Longrightarrow> thesis"
9.40      by (meson that)
9.41  qed
9.42 @@ -314,7 +314,7 @@
9.43
9.44      let ?f = "\<lambda>x. f x + b"
9.45      have "nn_integral M f \<noteq> top"
9.46 -      using f \<in> G[THEN G_D, of "space M"] by (auto simp: top_unique cong: nn_integral_cong)
9.47 +      using \<open>f \<in> G\<close>[THEN G_D, of "space M"] by (auto simp: top_unique cong: nn_integral_cong)
9.48      with \<open>b \<noteq> top\<close> interpret Mf: finite_measure "density M ?f"
9.49        by (intro finite_measureI)
9.50           (auto simp: field_simps mult_indicator_subset ennreal_mult_eq_top_iff

    10.1 --- a/src/HOL/Analysis/Set_Integral.thy	Tue Jan 17 11:26:21 2017 +0100
10.2 +++ b/src/HOL/Analysis/Set_Integral.thy	Tue Jan 17 13:59:10 2017 +0100
10.3 @@ -14,7 +14,7 @@
10.4  lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y" (* COPIED FROM Permutations *)
10.5    using surj_f_inv_f[of p] by (auto simp add: bij_def)
10.6
10.7 -subsection {*Fun.thy*}
10.8 +subsection \<open>Fun.thy\<close>
10.9
10.10  lemma inj_fn:
10.11    fixes f::"'a \<Rightarrow> 'a"
10.12 @@ -129,7 +129,7 @@
10.13    shows "Inf K \<in> K"
10.14  by (auto simp add: Min_def Inf_nat_def) (meson LeastI assms bot.extremum_unique subsetI)
10.15
10.16 -subsection {*Liminf-Limsup.thy*}
10.17 +subsection \<open>Liminf-Limsup.thy\<close>
10.18
10.19  lemma limsup_shift:
10.20    "limsup (\<lambda>n. u (n+1)) = limsup u"
10.21 @@ -140,7 +140,7 @@
10.22    have b: "(INF n. (SUP m:{n+1..}. u m)) = (INF n:{1..}. (SUP m:{n..}. u m))"
10.23      apply (rule INF_eq) using Suc_le_D by auto
10.24    have "(INF n:{1..}. v n) = (INF n. v n)" if "decseq v" for v::"nat \<Rightarrow> 'a"
10.25 -    apply (rule INF_eq) using decseq v decseq_Suc_iff by auto
10.26 +    apply (rule INF_eq) using \<open>decseq v\<close> decseq_Suc_iff by auto
10.27    moreover have "decseq (\<lambda>n. (SUP m:{n..}. u m))" by (simp add: SUP_subset_mono decseq_def)
10.28    ultimately have c: "(INF n:{1..}. (SUP m:{n..}. u m)) = (INF n. (SUP m:{n..}. u m))" by simp
10.29    have "(INF n. SUPREMUM {n..} u) = (INF n. SUP m:{n..}. u (m + 1))" using a b c by simp
10.30 @@ -164,7 +164,7 @@
10.31    have b: "(SUP n. (INF m:{n+1..}. u m)) = (SUP n:{1..}. (INF m:{n..}. u m))"
10.32      apply (rule SUP_eq) using Suc_le_D by (auto)
10.33    have "(SUP n:{1..}. v n) = (SUP n. v n)" if "incseq v" for v::"nat \<Rightarrow> 'a"
10.34 -    apply (rule SUP_eq) using incseq v incseq_Suc_iff by auto
10.35 +    apply (rule SUP_eq) using \<open>incseq v\<close> incseq_Suc_iff by auto
10.36    moreover have "incseq (\<lambda>n. (INF m:{n..}. u m))" by (simp add: INF_superset_mono mono_def)
10.37    ultimately have c: "(SUP n:{1..}. (INF m:{n..}. u m)) = (SUP n. (INF m:{n..}. u m))" by simp
10.38    have "(SUP n. INFIMUM {n..} u) = (SUP n. INF m:{n..}. u (m + 1))" using a b c by simp
10.39 @@ -188,8 +188,8 @@
10.40    then show ?thesis by (metis eventually_True mem_Collect_eq less_INF_D less_SUP_iff)
10.41  qed
10.42
10.43 -text {* The next lemma is extremely useful, as it often makes it possible to reduce statements
10.44 -about limsups to statements about limits.*}
10.45 +text \<open>The next lemma is extremely useful, as it often makes it possible to reduce statements
10.46 +about limsups to statements about limits.\<close>
10.47
10.48  lemma limsup_subseq_lim:
10.49    fixes u::"nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
10.50 @@ -203,12 +203,12 @@
10.51    define umax where "umax = (\<lambda>n. (SUP m:{n..}. u m))"
10.52    have "decseq umax" unfolding umax_def by (simp add: SUP_subset_mono antimono_def)
10.53    then have "umax \<longlonglongrightarrow> limsup u" unfolding umax_def by (metis LIMSEQ_INF limsup_INF_SUP)
10.54 -  then have *: "(umax o r) \<longlonglongrightarrow> limsup u" by (simp add: LIMSEQ_subseq_LIMSEQ subseq r)
10.55 +  then have *: "(umax o r) \<longlonglongrightarrow> limsup u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>subseq r\<close>)
10.56    have "\<And>n. umax(r n) = u(r n)" unfolding umax_def using mono
10.57      by (metis SUP_le_iff antisym atLeast_def mem_Collect_eq order_refl)
10.58    then have "umax o r = u o r" unfolding o_def by simp
10.59    then have "(u o r) \<longlonglongrightarrow> limsup u" using * by simp
10.60 -  then show ?thesis using subseq r by blast
10.61 +  then show ?thesis using \<open>subseq r\<close> by blast
10.62  next
10.63    assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. u m \<le> u p))"
10.64    then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. u p < u m" by (force simp: not_le le_less)
10.65 @@ -219,18 +219,18 @@
10.66      have "Max {u i |i. i \<in> {N<..x}} \<in> {u i |i. i \<in> {N<..x}}" apply (rule Max_in) using a by (auto)
10.67      then obtain p where "p \<in> {N<..x}" and upmax: "u p = Max{u i |i. i \<in> {N<..x}}" by auto
10.68      define U where "U = {m. m > p \<and> u p < u m}"
10.69 -    have "U \<noteq> {}" unfolding U_def using N[of p] p \<in> {N<..x} by auto
10.70 +    have "U \<noteq> {}" unfolding U_def using N[of p] \<open>p \<in> {N<..x}\<close> by auto
10.71      define y where "y = Inf U"
10.72 -    then have "y \<in> U" using U \<noteq> {} by (simp add: Inf_nat_def1)
10.73 +    then have "y \<in> U" using \<open>U \<noteq> {}\<close> by (simp add: Inf_nat_def1)
10.74      have a: "\<And>i. i \<in> {N<..x} \<Longrightarrow> u i \<le> u p"
10.75      proof -
10.76        fix i assume "i \<in> {N<..x}"
10.77        then have "u i \<in> {u i |i. i \<in> {N<..x}}" by blast
10.78        then show "u i \<le> u p" using upmax by simp
10.79      qed
10.80 -    moreover have "u p < u y" using y \<in> U U_def by auto
10.81 +    moreover have "u p < u y" using \<open>y \<in> U\<close> U_def by auto
10.82      ultimately have "y \<notin> {N<..x}" using not_le by blast
10.83 -    moreover have "y > N" using y \<in> U U_def p \<in> {N<..x} by auto
10.84 +    moreover have "y > N" using \<open>y \<in> U\<close> U_def \<open>p \<in> {N<..x}\<close> by auto
10.85      ultimately have "y > x" by auto
10.86
10.87      have "\<And>i. i \<in> {N<..y} \<Longrightarrow> u i \<le> u y"
10.88 @@ -241,7 +241,7 @@
10.89          then show ?thesis by simp
10.90        next
10.91          assume "\<not>(i=y)"
10.92 -        then have i:"i \<in> {N<..<y}" using i \<in> {N<..y} by simp
10.93 +        then have i:"i \<in> {N<..<y}" using \<open>i \<in> {N<..y}\<close> by simp
10.94          have "u i \<le> u p"
10.95          proof (cases)
10.96            assume "i \<le> x"
10.97 @@ -250,15 +250,15 @@
10.98          next
10.99            assume "\<not>(i \<le> x)"
10.100            then have "i > x" by simp
10.101 -          then have *: "i > p" using p \<in> {N<..x} by simp
10.102 +          then have *: "i > p" using \<open>p \<in> {N<..x}\<close> by simp
10.103            have "i < Inf U" using i y_def by simp
10.104            then have "i \<notin> U" using Inf_nat_def not_less_Least by auto
10.105            then show ?thesis using U_def * by auto
10.106          qed
10.107 -        then show "u i \<le> u y" using u p < u y by auto
10.108 +        then show "u i \<le> u y" using \<open>u p < u y\<close> by auto
10.109        qed
10.110      qed
10.111 -    then have "N < y \<and> x < y \<and> (\<forall>i\<in>{N<..y}. u i \<le> u y)" using y > x y > N by auto
10.112 +    then have "N < y \<and> x < y \<and> (\<forall>i\<in>{N<..y}. u i \<le> u y)" using \<open>y > x\<close> \<open>y > N\<close> by auto
10.113      then show "\<exists>y>N. x < y \<and> (\<forall>i\<in>{N<..y}. u i \<le> u y)" by auto
10.114    qed (auto)
10.115    then obtain r where r: "\<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<le> u (r (Suc n)))" by auto
10.116 @@ -266,12 +266,12 @@
10.117    have "incseq (u o r)" unfolding o_def using r by (simp add: incseq_SucI order.strict_implies_order)
10.118    then have "(u o r) \<longlonglongrightarrow> (SUP n. (u o r) n)" using LIMSEQ_SUP by blast
10.119    then have "limsup (u o r) = (SUP n. (u o r) n)" by (simp add: lim_imp_Limsup)
10.120 -  moreover have "limsup (u o r) \<le> limsup u" using subseq r by (simp add: limsup_subseq_mono)
10.121 +  moreover have "limsup (u o r) \<le> limsup u" using \<open>subseq r\<close> by (simp add: limsup_subseq_mono)
10.122    ultimately have "(SUP n. (u o r) n) \<le> limsup u" by simp
10.123
10.124    {
10.125      fix i assume i: "i \<in> {N<..}"
10.126 -    obtain n where "i < r (Suc n)" using subseq r using Suc_le_eq seq_suble by blast
10.127 +    obtain n where "i < r (Suc n)" using \<open>subseq r\<close> using Suc_le_eq seq_suble by blast
10.128      then have "i \<in> {N<..r(Suc n)}" using i by simp
10.129      then have "u i \<le> u (r(Suc n))" using r by simp
10.130      then have "u i \<le> (SUP n. (u o r) n)" unfolding o_def by (meson SUP_upper2 UNIV_I)
10.131 @@ -279,9 +279,9 @@
10.132    then have "(SUP i:{N<..}. u i) \<le> (SUP n. (u o r) n)" using SUP_least by blast
10.133    then have "limsup u \<le> (SUP n. (u o r) n)" unfolding Limsup_def
10.134      by (metis (mono_tags, lifting) INF_lower2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
10.135 -  then have "limsup u = (SUP n. (u o r) n)" using (SUP n. (u o r) n) \<le> limsup u by simp
10.136 -  then have "(u o r) \<longlonglongrightarrow> limsup u" using (u o r) \<longlonglongrightarrow> (SUP n. (u o r) n) by simp
10.137 -  then show ?thesis using subseq r by auto
10.138 +  then have "limsup u = (SUP n. (u o r) n)" using \<open>(SUP n. (u o r) n) \<le> limsup u\<close> by simp
10.139 +  then have "(u o r) \<longlonglongrightarrow> limsup u" using \<open>(u o r) \<longlonglongrightarrow> (SUP n. (u o r) n)\<close> by simp
10.140 +  then show ?thesis using \<open>subseq r\<close> by auto
10.141  qed
10.142
10.143  lemma liminf_subseq_lim:
10.144 @@ -296,12 +296,12 @@
10.145    define umin where "umin = (\<lambda>n. (INF m:{n..}. u m))"
10.146    have "incseq umin" unfolding umin_def by (simp add: INF_superset_mono incseq_def)
10.147    then have "umin \<longlonglongrightarrow> liminf u" unfolding umin_def by (metis LIMSEQ_SUP liminf_SUP_INF)
10.148 -  then have *: "(umin o r) \<longlonglongrightarrow> liminf u" by (simp add: LIMSEQ_subseq_LIMSEQ subseq r)
10.149 +  then have *: "(umin o r) \<longlonglongrightarrow> liminf u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>subseq r\<close>)
10.150    have "\<And>n. umin(r n) = u(r n)" unfolding umin_def using mono
10.151      by (metis le_INF_iff antisym atLeast_def mem_Collect_eq order_refl)
10.152    then have "umin o r = u o r" unfolding o_def by simp
10.153    then have "(u o r) \<longlonglongrightarrow> liminf u" using * by simp
10.154 -  then show ?thesis using subseq r by blast
10.155 +  then show ?thesis using \<open>subseq r\<close> by blast
10.156  next
10.157    assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. u m \<ge> u p))"
10.158    then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. u p > u m" by (force simp: not_le le_less)
10.159 @@ -312,18 +312,18 @@
10.160      have "Min {u i |i. i \<in> {N<..x}} \<in> {u i |i. i \<in> {N<..x}}" apply (rule Min_in) using a by (auto)
10.161      then obtain p where "p \<in> {N<..x}" and upmin: "u p = Min{u i |i. i \<in> {N<..x}}" by auto
10.162      define U where "U = {m. m > p \<and> u p > u m}"
10.163 -    have "U \<noteq> {}" unfolding U_def using N[of p] p \<in> {N<..x} by auto
10.164 +    have "U \<noteq> {}" unfolding U_def using N[of p] \<open>p \<in> {N<..x}\<close> by auto
10.165      define y where "y = Inf U"
10.166 -    then have "y \<in> U" using U \<noteq> {} by (simp add: Inf_nat_def1)
10.167 +    then have "y \<in> U" using \<open>U \<noteq> {}\<close> by (simp add: Inf_nat_def1)
10.168      have a: "\<And>i. i \<in> {N<..x} \<Longrightarrow> u i \<ge> u p"
10.169      proof -
10.170        fix i assume "i \<in> {N<..x}"
10.171        then have "u i \<in> {u i |i. i \<in> {N<..x}}" by blast
10.172        then show "u i \<ge> u p" using upmin by simp
10.173      qed
10.174 -    moreover have "u p > u y" using y \<in> U U_def by auto
10.175 +    moreover have "u p > u y" using \<open>y \<in> U\<close> U_def by auto
10.176      ultimately have "y \<notin> {N<..x}" using not_le by blast
10.177 -    moreover have "y > N" using y \<in> U U_def p \<in> {N<..x} by auto
10.178 +    moreover have "y > N" using \<open>y \<in> U\<close> U_def \<open>p \<in> {N<..x}\<close> by auto
10.179      ultimately have "y > x" by auto
10.180
10.181      have "\<And>i. i \<in> {N<..y} \<Longrightarrow> u i \<ge> u y"
10.182 @@ -334,7 +334,7 @@
10.183          then show ?thesis by simp
10.184        next
10.185          assume "\<not>(i=y)"
10.186 -        then have i:"i \<in> {N<..<y}" using i \<in> {N<..y} by simp
10.187 +        then have i:"i \<in> {N<..<y}" using \<open>i \<in> {N<..y}\<close> by simp
10.188          have "u i \<ge> u p"
10.189          proof (cases)
10.190            assume "i \<le> x"
10.191 @@ -343,15 +343,15 @@
10.192          next
10.193            assume "\<not>(i \<le> x)"
10.194            then have "i > x" by simp
10.195 -          then have *: "i > p" using p \<in> {N<..x} by simp
10.196 +          then have *: "i > p" using \<open>p \<in> {N<..x}\<close> by simp
10.197            have "i < Inf U" using i y_def by simp
10.198            then have "i \<notin> U" using Inf_nat_def not_less_Least by auto
10.199            then show ?thesis using U_def * by auto
10.200          qed
10.201 -        then show "u i \<ge> u y" using u p > u y by auto
10.202 +        then show "u i \<ge> u y" using \<open>u p > u y\<close> by auto
10.203        qed
10.204      qed
10.205 -    then have "N < y \<and> x < y \<and> (\<forall>i\<in>{N<..y}. u i \<ge> u y)" using y > x y > N by auto
10.206 +    then have "N < y \<and> x < y \<and> (\<forall>i\<in>{N<..y}. u i \<ge> u y)" using \<open>y > x\<close> \<open>y > N\<close> by auto
10.207      then show "\<exists>y>N. x < y \<and> (\<forall>i\<in>{N<..y}. u i \<ge> u y)" by auto
10.208    qed (auto)
10.209    then obtain r where r: "\<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<ge> u (r (Suc n)))" by auto
10.210 @@ -359,12 +359,12 @@
10.211    have "decseq (u o r)" unfolding o_def using r by (simp add: decseq_SucI order.strict_implies_order)
10.212    then have "(u o r) \<longlonglongrightarrow> (INF n. (u o r) n)" using LIMSEQ_INF by blast
10.213    then have "liminf (u o r) = (INF n. (u o r) n)" by (simp add: lim_imp_Liminf)
10.214 -  moreover have "liminf (u o r) \<ge> liminf u" using subseq r by (simp add: liminf_subseq_mono)
10.215 +  moreover have "liminf (u o r) \<ge> liminf u" using \<open>subseq r\<close> by (simp add: liminf_subseq_mono)
10.216    ultimately have "(INF n. (u o r) n) \<ge> liminf u" by simp
10.217
10.218    {
10.219      fix i assume i: "i \<in> {N<..}"
10.220 -    obtain n where "i < r (Suc n)" using subseq r using Suc_le_eq seq_suble by blast
10.221 +    obtain n where "i < r (Suc n)" using \<open>subseq r\<close> using Suc_le_eq seq_suble by blast
10.222      then have "i \<in> {N<..r(Suc n)}" using i by simp
10.223      then have "u i \<ge> u (r(Suc n))" using r by simp
10.224      then have "u i \<ge> (INF n. (u o r) n)" unfolding o_def by (meson INF_lower2 UNIV_I)
10.225 @@ -372,15 +372,15 @@
10.226    then have "(INF i:{N<..}. u i) \<ge> (INF n. (u o r) n)" using INF_greatest by blast
10.227    then have "liminf u \<ge> (INF n. (u o r) n)" unfolding Liminf_def
10.228      by (metis (mono_tags, lifting) SUP_upper2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
10.229 -  then have "liminf u = (INF n. (u o r) n)" using (INF n. (u o r) n) \<ge> liminf u by simp
10.230 -  then have "(u o r) \<longlonglongrightarrow> liminf u" using (u o r) \<longlonglongrightarrow> (INF n. (u o r) n) by simp
10.231 -  then show ?thesis using subseq r by auto
10.232 +  then have "liminf u = (INF n. (u o r) n)" using \<open>(INF n. (u o r) n) \<ge> liminf u\<close> by simp
10.233 +  then have "(u o r) \<longlonglongrightarrow> liminf u" using \<open>(u o r) \<longlonglongrightarrow> (INF n. (u o r) n)\<close> by simp
10.234 +  then show ?thesis using \<open>subseq r\<close> by auto
10.235  qed
10.236
10.237
10.238 -subsection {*Extended-Real.thy*}
10.239 +subsection \<open>Extended-Real.thy\<close>
10.240
10.241 -text{* The proof of this one is copied from \verb+ereal_add_mono+. *}
10.242 +text\<open>The proof of this one is copied from \verb+ereal_add_mono+.\<close>
10.244    fixes a b c d :: ereal
10.245    assumes "a < b"
10.246 @@ -392,7 +392,7 @@
10.247  apply (cases rule: ereal3_cases[of b c d], auto)
10.248  done
10.249
10.250 -text {* The next ones are analogues of \verb+mult_mono+ and \verb+mult_mono'+ in ereal.*}
10.251 +text \<open>The next ones are analogues of \verb+mult_mono+ and \verb+mult_mono'+ in ereal.\<close>
10.252
10.253  lemma ereal_mult_mono:
10.254    fixes a b c d::ereal
10.255 @@ -411,7 +411,7 @@
10.256    assumes "b > 0" "c > 0" "a < b" "c < d"
10.257    shows "a * c < b * d"
10.258  proof -
10.259 -  have "c < \<infinity>" using c < d by auto
10.260 +  have "c < \<infinity>" using \<open>c < d\<close> by auto
10.261    then have "a * c < b * c" by (metis ereal_mult_strict_left_mono[OF assms(3) assms(2)] mult.commute)
10.262    moreover have "b * c \<le> b * d" using assms(2) assms(4) by (simp add: assms(1) ereal_mult_left_mono less_imp_le)
10.263    ultimately show ?thesis by simp
10.264 @@ -465,13 +465,13 @@
10.265  qed
10.266
10.267
10.268 -subsubsection {*Continuity of addition*}
10.269 +subsubsection \<open>Continuity of addition\<close>
10.270
10.271 -text {*The next few lemmas remove an unnecessary assumption in \verb+tendsto_add_ereal+, culminating
10.272 +text \<open>The next few lemmas remove an unnecessary assumption in \verb+tendsto_add_ereal+, culminating
10.273  in \verb+tendsto_add_ereal_general+ which essentially says that the addition
10.274  is continuous on ereal times ereal, except at $(-\infty, \infty)$ and $(\infty, -\infty)$.
10.275  It is much more convenient in many situations, see for instance the proof of
10.276 -\verb+tendsto_sum_ereal+ below. *}
10.277 +\verb+tendsto_sum_ereal+ below.\<close>
10.278
10.280    fixes y :: ereal
10.281 @@ -507,9 +507,9 @@
10.282    then show ?thesis by (simp add: tendsto_PInfty)
10.283  qed
10.284
10.285 -text{* One would like to deduce the next lemma from the previous one, but the fact
10.286 +text\<open>One would like to deduce the next lemma from the previous one, but the fact
10.287  that $-(x+y)$ is in general different from $(-x) + (-y)$ in ereal creates difficulties,
10.288 -so it is more efficient to copy the previous proof.*}
10.289 +so it is more efficient to copy the previous proof.\<close>
10.290
10.292    fixes y :: ereal
10.293 @@ -574,8 +574,8 @@
10.294    ultimately show ?thesis by simp
10.295  qed
10.296
10.297 -text {* The next lemma says that the addition is continuous on ereal, except at
10.298 -the pairs $(-\infty, \infty)$ and $(\infty, -\infty)$. *}
10.299 +text \<open>The next lemma says that the addition is continuous on ereal, except at
10.300 +the pairs $(-\infty, \infty)$ and $(\infty, -\infty)$.\<close>
10.301
10.302  lemma tendsto_add_ereal_general [tendsto_intros]:
10.303    fixes x y :: ereal
10.304 @@ -596,11 +596,11 @@
10.305    then show ?thesis using tendsto_add_ereal_MInf MInf f g by (metis ereal_MInfty_eq_plus)
10.306  qed
10.307
10.308 -subsubsection {*Continuity of multiplication*}
10.309 +subsubsection \<open>Continuity of multiplication\<close>
10.310
10.311 -text {* In the same way as for addition, we prove that the multiplication is continuous on
10.312 +text \<open>In the same way as for addition, we prove that the multiplication is continuous on
10.313  ereal times ereal, except at $(\infty, 0)$ and $(-\infty, 0)$ and $(0, \infty)$ and $(0, -\infty)$,
10.314 -starting with specific situations.*}
10.315 +starting with specific situations.\<close>
10.316
10.317  lemma tendsto_mult_real_ereal:
10.318    assumes "(u \<longlongrightarrow> ereal l) F" "(v \<longlongrightarrow> ereal m) F"
10.319 @@ -631,15 +631,15 @@
10.320    shows "((\<lambda>x. f x * g x) \<longlongrightarrow> \<infinity>) F"
10.321  proof -
10.322    obtain a::real where "0 < ereal a" "a < l" using assms(2) using ereal_dense2 by blast
10.323 -  have *: "eventually (\<lambda>x. f x > a) F" using a < l assms(1) by (simp add: order_tendsto_iff)
10.324 +  have *: "eventually (\<lambda>x. f x > a) F" using \<open>a < l\<close> assms(1) by (simp add: order_tendsto_iff)
10.325    {
10.326      fix K::real
10.327      define M where "M = max K 1"
10.328      then have "M > 0" by simp
10.329 -    then have "ereal(M/a) > 0" using ereal a > 0 by simp
10.330 +    then have "ereal(M/a) > 0" using \<open>ereal a > 0\<close> by simp
10.331      then have "\<And>x. ((f x > a) \<and> (g x > M/a)) \<Longrightarrow> (f x * g x > ereal a * ereal(M/a))"
10.332 -      using ereal_mult_mono_strict'[where ?c = "M/a", OF 0 < ereal a] by auto
10.333 -    moreover have "ereal a * ereal(M/a) = M" using ereal a > 0 by simp
10.334 +      using ereal_mult_mono_strict'[where ?c = "M/a", OF \<open>0 < ereal a\<close>] by auto
10.335 +    moreover have "ereal a * ereal(M/a) = M" using \<open>ereal a > 0\<close> by simp
10.336      ultimately have "\<And>x. ((f x > a) \<and> (g x > M/a)) \<Longrightarrow> (f x * g x > M)" by simp
10.337      moreover have "M \<ge> K" unfolding M_def by simp
10.338      ultimately have Imp: "\<And>x. ((f x > a) \<and> (g x > M/a)) \<Longrightarrow> (f x * g x > K)"
10.339 @@ -674,13 +674,13 @@
10.340    assume "\<not>(l = \<infinity> \<or> m = \<infinity>)"
10.341    then have "l < \<infinity>" "m < \<infinity>" by auto
10.342    then obtain lr mr where "l = ereal lr" "m = ereal mr"
10.343 -    using l>0 m>0 by (metis ereal_cases ereal_less(6) not_less_iff_gr_or_eq)
10.344 +    using \<open>l>0\<close> \<open>m>0\<close> by (metis ereal_cases ereal_less(6) not_less_iff_gr_or_eq)
10.345    then show ?thesis using tendsto_mult_real_ereal assms by auto
10.346  qed
10.347
10.348 -text {*We reduce the general situation to the positive case by multiplying by suitable signs.
10.349 +text \<open>We reduce the general situation to the positive case by multiplying by suitable signs.
10.350  Unfortunately, as ereal is not a ring, all the neat sign lemmas are not available there. We
10.351 -give the bare minimum we need.*}
10.352 +give the bare minimum we need.\<close>
10.353
10.354  lemma ereal_sgn_abs:
10.355    fixes l::ereal
10.356 @@ -720,9 +720,9 @@
10.357    have "((\<lambda>x. (sgn(l) * sgn(m)) * ((sgn(l) * f x) * (sgn(m) * g x))) \<longlongrightarrow> (sgn(l) * sgn(m)) * ((sgn(l) * l) * (sgn(m) * m))) F"
10.358      by (rule tendsto_cmult_ereal, auto simp add: sgn_finite2 *)
10.359    moreover have "\<And>x. (sgn(l) * sgn(m)) * ((sgn(l) * f x) * (sgn(m) * g x)) = f x * g x"
10.360 -    by (metis mult.left_neutral sgn_squared_ereal[OF l \<noteq> 0] sgn_squared_ereal[OF m \<noteq> 0] mult.assoc mult.commute)
10.361 +    by (metis mult.left_neutral sgn_squared_ereal[OF \<open>l \<noteq> 0\<close>] sgn_squared_ereal[OF \<open>m \<noteq> 0\<close>] mult.assoc mult.commute)
10.362    moreover have "(sgn(l) * sgn(m)) * ((sgn(l) * l) * (sgn(m) * m)) = l * m"
10.363 -    by (metis mult.left_neutral sgn_squared_ereal[OF l \<noteq> 0] sgn_squared_ereal[OF m \<noteq> 0] mult.assoc mult.commute)
10.364 +    by (metis mult.left_neutral sgn_squared_ereal[OF \<open>l \<noteq> 0\<close>] sgn_squared_ereal[OF \<open>m \<noteq> 0\<close>] mult.assoc mult.commute)
10.365    ultimately show ?thesis by auto
10.366  qed
10.367
10.368 @@ -733,7 +733,7 @@
10.369  by (cases "c = 0", auto simp add: assms tendsto_mult_ereal)
10.370
10.371
10.372 -subsubsection {*Continuity of division*}
10.373 +subsubsection \<open>Continuity of division\<close>
10.374
10.375  lemma tendsto_inverse_ereal_PInf:
10.376    fixes u::"_ \<Rightarrow> ereal"
10.377 @@ -747,9 +747,9 @@
10.378      moreover
10.379      {
10.380        fix z::ereal assume "z>1/e"
10.381 -      then have "z>0" using e>0 using less_le_trans not_le by fastforce
10.382 +      then have "z>0" using \<open>e>0\<close> using less_le_trans not_le by fastforce
10.383        then have "1/z \<ge> 0" by auto
10.384 -      moreover have "1/z < e" using e>0 z>1/e
10.385 +      moreover have "1/z < e" using \<open>e>0\<close> \<open>z>1/e\<close>
10.386          apply (cases z) apply auto
10.387          by (metis (mono_tags, hide_lams) less_ereal.simps(2) less_ereal.simps(4) divide_less_eq ereal_divide_less_pos ereal_less(4)
10.388              ereal_less_eq(4) less_le_trans mult_eq_0_iff not_le not_one_less_zero times_ereal.simps(1))
10.389 @@ -765,11 +765,11 @@
10.390      fix a::ereal assume "a>0"
10.391      then obtain e::real where "e>0" "a>e" using ereal_dense2 ereal_less(2) by blast
10.392      then have "eventually (\<lambda>n. 1/u n < e) F" using *(1) by auto
10.393 -    then show "eventually (\<lambda>n. 1/u n < a) F" using a>e by (metis (mono_tags, lifting) eventually_mono less_trans)
10.394 +    then show "eventually (\<lambda>n. 1/u n < a) F" using \<open>a>e\<close> by (metis (mono_tags, lifting) eventually_mono less_trans)
10.395    qed
10.396  qed
10.397
10.398 -text {* The next lemma deserves to exist by itself, as it is so common and useful. *}
10.399 +text \<open>The next lemma deserves to exist by itself, as it is so common and useful.\<close>
10.400
10.401  lemma tendsto_inverse_real [tendsto_intros]:
10.402    fixes u::"_ \<Rightarrow> real"
10.403 @@ -836,7 +836,7 @@
10.404  qed
10.405
10.406
10.407 -subsubsection {*Further limits*}
10.408 +subsubsection \<open>Further limits\<close>
10.409
10.410  lemma id_nat_ereal_tendsto_PInf [tendsto_intros]:
10.411    "(\<lambda> n::nat. real n) \<longlonglongrightarrow> \<infinity>"
10.412 @@ -860,8 +860,8 @@
10.413        proof (rule ccontr)
10.414          assume "\<not>(N > C)"
10.415          have "u N \<le> Max {u n| n. n \<le> C}"
10.416 -          apply (rule Max_ge) using \<not>(N > C) by auto
10.417 -        then show False using u N \<ge> n n \<ge> M unfolding M_def by auto
10.418 +          apply (rule Max_ge) using \<open>\<not>(N > C)\<close> by auto
10.419 +        then show False using \<open>u N \<ge> n\<close> \<open>n \<ge> M\<close> unfolding M_def by auto
10.420        qed
10.421        then have **: "{N. u N \<ge> n} \<subseteq> {C..}" by fastforce
10.422        have "Inf {N. u N \<ge> n} \<ge> C"
10.423 @@ -981,7 +981,7 @@
10.424    ultimately show ?thesis using MInf by auto
10.425  qed (simp add: assms)
10.426
10.427 -text {* the next one is copied from \verb+tendsto_sum+. *}
10.428 +text \<open>the next one is copied from \verb+tendsto_sum+.\<close>
10.429  lemma tendsto_sum_ereal [tendsto_intros]:
10.430    fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ereal"
10.431    assumes "\<And>i. i \<in> S \<Longrightarrow> (f i \<longlongrightarrow> a i) F"
10.432 @@ -992,7 +992,7 @@
10.433      by (induct, simp, simp add: tendsto_add_ereal_general2 assms)
10.434  qed(simp)
10.435
10.436 -subsubsection {*Limsups and liminfs*}
10.437 +subsubsection \<open>Limsups and liminfs\<close>
10.438
10.439  lemma limsup_finite_then_bounded:
10.440    fixes u::"nat \<Rightarrow> real"
10.441 @@ -1017,7 +1017,7 @@
10.442        assume "\<not>(n \<le> N)"
10.443        then have "n \<ge> N" by simp
10.444        then have "u n < C" using N by auto
10.445 -      then have "u n < real_of_ereal C" using C = ereal(real_of_ereal C) less_ereal.simps(1) by fastforce
10.446 +      then have "u n < real_of_ereal C" using \<open>C = ereal(real_of_ereal C)\<close> less_ereal.simps(1) by fastforce
10.447        then show "u n \<le> D" unfolding D_def by linarith
10.448      qed
10.449    qed
10.450 @@ -1047,7 +1047,7 @@
10.451        assume "\<not>(n \<le> N)"
10.452        then have "n \<ge> N" by simp
10.453        then have "u n > C" using N by auto
10.454 -      then have "u n > real_of_ereal C" using C = ereal(real_of_ereal C) less_ereal.simps(1) by fastforce
10.455 +      then have "u n > real_of_ereal C" using \<open>C = ereal(real_of_ereal C)\<close> less_ereal.simps(1) by fastforce
10.456        then show "u n \<ge> D" unfolding D_def by linarith
10.457      qed
10.458    qed
10.459 @@ -1060,9 +1060,9 @@
10.460    shows "\<exists>N>k. u N < l"
10.461  by (metis assms gt_ex less_le_trans liminf_bounded_iff not_less)
10.462
10.463 -text {* The following statement about limsups is reduced to a statement about limits using
10.464 +text \<open>The following statement about limsups is reduced to a statement about limits using
10.465  subsequences thanks to \verb+limsup_subseq_lim+. The statement for limits follows for instance from
10.468
10.470    fixes u v::"nat \<Rightarrow> ereal"
10.471 @@ -1091,9 +1091,9 @@
10.472    done
10.473
10.474    have "limsup (u o r) \<le> limsup u" by (simp add: limsup_subseq_mono r(1))
10.475 -  then have a: "limsup (u o r) \<noteq> \<infinity>" using limsup u < \<infinity> by auto
10.476 +  then have a: "limsup (u o r) \<noteq> \<infinity>" using \<open>limsup u < \<infinity>\<close> by auto
10.477    have "limsup (v o r o s) \<le> limsup v" by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) subseq_o)
10.478 -  then have b: "limsup (v o r o s) \<noteq> \<infinity>" using limsup v < \<infinity> by auto
10.479 +  then have b: "limsup (v o r o s) \<noteq> \<infinity>" using \<open>limsup v < \<infinity>\<close> by auto
10.480
10.481    have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> limsup (u o r) + limsup (v o r o s)"
10.482      using l tendsto_add_ereal_general a b by fastforce
10.483 @@ -1101,13 +1101,13 @@
10.484    ultimately have "(w o a) \<longlonglongrightarrow> limsup (u o r) + limsup (v o r o s)" by simp
10.485    then have "limsup w = limsup (u o r) + limsup (v o r o s)" using l(1) LIMSEQ_unique by blast
10.486    then have "limsup w \<le> limsup u + limsup v"
10.487 -    using limsup (u o r) \<le> limsup u limsup (v o r o s) \<le> limsup v ereal_add_mono by simp
10.488 +    using \<open>limsup (u o r) \<le> limsup u\<close> \<open>limsup (v o r o s) \<le> limsup v\<close> ereal_add_mono by simp
10.489    then show ?thesis unfolding w_def by simp
10.490  qed
10.491
10.492 -text {* There is an asymmetry between liminfs and limsups in ereal, as $\infty + (-\infty) = \infty$.
10.493 +text \<open>There is an asymmetry between liminfs and limsups in ereal, as $\infty + (-\infty) = \infty$.
10.494  This explains why there are more assumptions in the next lemma dealing with liminfs that in the
10.495 -previous one about limsups.*}
10.496 +previous one about limsups.\<close>
10.497
10.499    fixes u v::"nat \<Rightarrow> ereal"
10.500 @@ -1137,9 +1137,9 @@
10.501    done
10.502
10.503    have "liminf (u o r) \<ge> liminf u" by (simp add: liminf_subseq_mono r(1))
10.504 -  then have a: "liminf (u o r) \<noteq> -\<infinity>" using liminf u > -\<infinity> by auto
10.505 +  then have a: "liminf (u o r) \<noteq> -\<infinity>" using \<open>liminf u > -\<infinity>\<close> by auto
10.506    have "liminf (v o r o s) \<ge> liminf v" by (simp add: comp_assoc liminf_subseq_mono r(1) s(1) subseq_o)
10.507 -  then have b: "liminf (v o r o s) \<noteq> -\<infinity>" using liminf v > -\<infinity> by auto
10.508 +  then have b: "liminf (v o r o s) \<noteq> -\<infinity>" using \<open>liminf v > -\<infinity>\<close> by auto
10.509
10.510    have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> liminf (u o r) + liminf (v o r o s)"
10.511      using l tendsto_add_ereal_general a b by fastforce
10.512 @@ -1147,7 +1147,7 @@
10.513    ultimately have "(w o a) \<longlonglongrightarrow> liminf (u o r) + liminf (v o r o s)" by simp
10.514    then have "liminf w = liminf (u o r) + liminf (v o r o s)" using l(1) LIMSEQ_unique by blast
10.515    then have "liminf w \<ge> liminf u + liminf v"
10.516 -    using liminf (u o r) \<ge> liminf u liminf (v o r o s) \<ge> liminf v ereal_add_mono by simp
10.517 +    using \<open>liminf (u o r) \<ge> liminf u\<close> \<open>liminf (v o r o s) \<ge> liminf v\<close> ereal_add_mono by simp
10.518    then show ?thesis unfolding w_def by simp
10.519  qed
10.520
10.521 @@ -1162,7 +1162,7 @@
10.522
10.523    have "limsup (\<lambda>n. u n + v n) \<le> limsup u + limsup v"
10.524      by (rule ereal_limsup_add_mono)
10.525 -  then have up: "limsup (\<lambda>n. u n + v n) \<le> a + limsup v" using limsup u = a by simp
10.526 +  then have up: "limsup (\<lambda>n. u n + v n) \<le> a + limsup v" using \<open>limsup u = a\<close> by simp
10.527
10.528    have a: "limsup (\<lambda>n. (u n + v n) + (-u n)) \<le> limsup (\<lambda>n. u n + v n) + limsup (\<lambda>n. -u n)"
10.529      by (rule ereal_limsup_add_mono)
10.530 @@ -1177,7 +1177,7 @@
10.531    ultimately have "eventually (\<lambda>n. u n + v n + (-u n) = v n) sequentially"
10.532      using eventually_mono by force
10.533    then have "limsup v = limsup (\<lambda>n. u n + v n + (-u n))" using Limsup_eq by force
10.534 -  then have "limsup v \<le> limsup (\<lambda>n. u n + v n) -a" using a limsup (\<lambda>n. -u n) = -a by (simp add: minus_ereal_def)
10.535 +  then have "limsup v \<le> limsup (\<lambda>n. u n + v n) -a" using a \<open>limsup (\<lambda>n. -u n) = -a\<close> by (simp add: minus_ereal_def)
10.536    then have "limsup (\<lambda>n. u n + v n) \<ge> a + limsup v" using assms(2) by (metis add.commute ereal_le_minus)
10.537    then show ?thesis using up by simp
10.538  qed
10.539 @@ -1255,7 +1255,7 @@
10.540
10.541    have "liminf (\<lambda>n. u n + v n) \<ge> liminf u + liminf v"
10.542      apply (rule ereal_liminf_add_mono) using * by auto
10.543 -  then have up: "liminf (\<lambda>n. u n + v n) \<ge> a + liminf v" using liminf u = a by simp
10.544 +  then have up: "liminf (\<lambda>n. u n + v n) \<ge> a + liminf v" using \<open>liminf u = a\<close> by simp
10.545
10.546    have a: "liminf (\<lambda>n. (u n + v n) + (-u n)) \<ge> liminf (\<lambda>n. u n + v n) + liminf (\<lambda>n. -u n)"
10.547      apply (rule ereal_liminf_add_mono) using ** by auto
10.548 @@ -1270,7 +1270,7 @@
10.549    ultimately have "eventually (\<lambda>n. u n + v n + (-u n) = v n) sequentially"
10.550      using eventually_mono by force
10.551    then have "liminf v = liminf (\<lambda>n. u n + v n + (-u n))" using Liminf_eq by force
10.552 -  then have "liminf v \<ge> liminf (\<lambda>n. u n + v n) -a" using a liminf (\<lambda>n. -u n) = -a by (simp add: minus_ereal_def)
10.553 +  then have "liminf v \<ge> liminf (\<lambda>n. u n + v n) -a" using a \<open>liminf (\<lambda>n. -u n) = -a\<close> by (simp add: minus_ereal_def)
10.554    then have "liminf (\<lambda>n. u n + v n) \<le> a + liminf v" using assms(2) by (metis add.commute ereal_minus_le)
10.555    then show ?thesis using up by simp
10.556  qed
10.557 @@ -1302,15 +1302,15 @@
10.558
10.559    have "liminf (w o r) \<ge> liminf w" by (simp add: liminf_subseq_mono r(1))
10.560    have "limsup (v o r o s) \<le> limsup v" by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) subseq_o)
10.561 -  then have b: "limsup (v o r o s) < \<infinity>" using limsup v < \<infinity> by auto
10.562 +  then have b: "limsup (v o r o s) < \<infinity>" using \<open>limsup v < \<infinity>\<close> by auto
10.563
10.564    have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> liminf u + limsup (v o r o s)"
10.565 -    apply (rule tendsto_add_ereal_general) using b liminf u < \<infinity> l(1) l(3) by force+
10.566 +    apply (rule tendsto_add_ereal_general) using b \<open>liminf u < \<infinity>\<close> l(1) l(3) by force+
10.567    moreover have "(\<lambda>n. (u o a) n + (v o a) n) = (w o a)" unfolding w_def by auto
10.568    ultimately have "(w o a) \<longlonglongrightarrow> liminf u + limsup (v o r o s)" by simp
10.569    then have "liminf (w o r) = liminf u + limsup (v o r o s)" using l(2) using LIMSEQ_unique by blast
10.570    then have "liminf w \<le> liminf u + limsup v"
10.571 -    using liminf (w o r) \<ge> liminf w limsup (v o r o s) \<le> limsup v
10.572 +    using \<open>liminf (w o r) \<ge> liminf w\<close> \<open>limsup (v o r o s) \<le> limsup v\<close>
10.573      by (metis add_mono_thms_linordered_semiring(2) le_less_trans not_less)
10.574    then show ?thesis unfolding w_def by simp
10.575  qed
10.576 @@ -1858,8 +1858,8 @@
10.577    by (rule set_borel_measurable_continuous[OF _ assms]) simp
10.578
10.579
10.580 -text{* This notation is from Sébastien Gouëzel: His use is not directly in line with the
10.581 -notations in this file, they are more in line with sum, and more readable he thinks. *}
10.582 +text\<open>This notation is from Sébastien Gouëzel: His use is not directly in line with the
10.583 +notations in this file, they are more in line with sum, and more readable he thinks.\<close>
10.584
10.585  abbreviation "set_nn_integral M A f \<equiv> nn_integral M (\<lambda>x. f x * indicator A x)"
10.586
10.587 @@ -1921,7 +1921,7 @@
10.588      assume "x \<in> (\<Union>n. B n)"
10.589      then obtain n where "x \<in> B n" by blast
10.590      have a: "finite {n}" by simp
10.591 -    have "\<And>i. i \<noteq> n \<Longrightarrow> x \<notin> B i" using x \<in> B n assms(3) disjoint_family_on_def
10.592 +    have "\<And>i. i \<noteq> n \<Longrightarrow> x \<notin> B i" using \<open>x \<in> B n\<close> assms(3) disjoint_family_on_def
10.593        by (metis IntI UNIV_I empty_iff)
10.594      then have "\<And>i. i \<notin> {n} \<Longrightarrow> indicator (B i) x = (0::ennreal)" using indicator_def by simp
10.595      then have b: "\<And>i. i \<notin> {n} \<Longrightarrow> f x * indicator (B i) x = (0::ennreal)" by simp
10.596 @@ -1932,14 +1932,14 @@
10.597        by (metis sums_unique[OF sums_finite[OF a]])
10.598      then have "(\<Sum>i. h i) = h n" by simp
10.599      then have "(\<Sum>n. f x * indicator (B n) x) = f x * indicator (B n) x" using h_def by simp
10.600 -    then have "(\<Sum>n. f x * indicator (B n) x) = f x" using x \<in> B n indicator_def by simp
10.601 -    then show ?thesis using x \<in> (\<Union>n. B n) by auto
10.602 +    then have "(\<Sum>n. f x * indicator (B n) x) = f x" using \<open>x \<in> B n\<close> indicator_def by simp
10.603 +    then show ?thesis using \<open>x \<in> (\<Union>n. B n)\<close> by auto
10.604    next
10.605      assume "x \<notin> (\<Union>n. B n)"
10.606      then have "\<And>n. f x * indicator (B n) x = 0" by simp
10.607      have "(\<Sum>n. f x * indicator (B n) x) = 0"
10.608 -      by (simp add: \<And>n. f x * indicator (B n) x = 0)
10.609 -    then show ?thesis using x \<notin> (\<Union>n. B n) by auto
10.610 +      by (simp add: \<open>\<And>n. f x * indicator (B n) x = 0\<close>)
10.611 +    then show ?thesis using \<open>x \<notin> (\<Union>n. B n)\<close> by auto
10.612    qed
10.613    ultimately show ?thesis by simp
10.614  qed
10.615 @@ -2035,14 +2035,14 @@
10.616  proof -
10.617    have "AE x in M. indicator A x * f x = 0"
10.618      apply (subst integral_nonneg_eq_0_iff_AE[symmetric])
10.619 -    using assms integrable_mult_indicator[OF A \<in> sets M assms(1)] by auto
10.620 +    using assms integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
10.621    then have "AE x\<in>A in M. f x = 0" by auto
10.622    then have "AE x\<in>A in M. False" using assms(3) by auto
10.623    then show "A \<in> null_sets M" using assms(2) by (simp add: AE_iff_null_sets)
10.624  qed
10.625
10.626 -text{*The next lemma is a variant of \<open>density_unique\<close>. Note that it uses the notation
10.627 -for nonnegative set integrals introduced earlier.*}
10.628 +text\<open>The next lemma is a variant of \<open>density_unique\<close>. Note that it uses the notation
10.629 +for nonnegative set integrals introduced earlier.\<close>
10.630
10.631  lemma (in sigma_finite_measure) density_unique2:
10.632    assumes [measurable]: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
10.633 @@ -2054,9 +2054,9 @@
10.634  qed (auto simp add: assms)
10.635
10.636
10.637 -text {* The next lemma implies the same statement for Banach-space valued functions
10.638 +text \<open>The next lemma implies the same statement for Banach-space valued functions
10.639  using Hahn-Banach theorem and linear forms. Since they are not yet easily available, I
10.640 -only formulate it for real-valued functions.*}
10.641 +only formulate it for real-valued functions.\<close>
10.642
10.643  lemma density_unique_real:
10.644    fixes f f'::"_ \<Rightarrow> real"
10.645 @@ -2067,7 +2067,7 @@
10.646    define A where "A = {x \<in> space M. f x < f' x}"
10.647    then have [measurable]: "A \<in> sets M" by simp
10.648    have "(\<integral>x \<in> A. (f' x - f x) \<partial>M) = (\<integral>x \<in> A. f' x \<partial>M) - (\<integral>x \<in> A. f x \<partial>M)"
10.649 -    using A \<in> sets M assms(1) assms(2) integrable_mult_indicator by blast
10.650 +    using \<open>A \<in> sets M\<close> assms(1) assms(2) integrable_mult_indicator by blast
10.651    then have "(\<integral>x \<in> A. (f' x - f x) \<partial>M) = 0" using assms(3) by simp
10.652    then have "A \<in> null_sets M"
10.653      using A_def null_if_pos_func_has_zero_int[where ?f = "\<lambda>x. f' x - f x" and ?A = A] assms by auto
10.654 @@ -2078,7 +2078,7 @@
10.655    define B where "B = {x \<in> space M. f' x < f x}"
10.656    then have [measurable]: "B \<in> sets M" by simp
10.657    have "(\<integral>x \<in> B. (f x - f' x) \<partial>M) = (\<integral>x \<in> B. f x \<partial>M) - (\<integral>x \<in> B. f' x \<partial>M)"
10.658 -    using B \<in> sets M assms(1) assms(2) integrable_mult_indicator by blast
10.659 +    using \<open>B \<in> sets M\<close> assms(1) assms(2) integrable_mult_indicator by blast
10.660    then have "(\<integral>x \<in> B. (f x - f' x) \<partial>M) = 0" using assms(3) by simp
10.661    then have "B \<in> null_sets M"
10.662      using B_def null_if_pos_func_has_zero_int[where ?f = "\<lambda>x. f x - f' x" and ?A = B] assms by auto
10.663 @@ -2088,13 +2088,13 @@
10.664    then show ?thesis using * by auto
10.665  qed
10.666
10.667 -text {* The next lemma shows that $L^1$ convergence of a sequence of functions follows from almost
10.668 +text \<open>The next lemma shows that $L^1$ convergence of a sequence of functions follows from almost
10.669  everywhere convergence and the weaker condition of the convergence of the integrated norms (or even
10.670  just the nontrivial inequality about them). Useful in a lot of contexts! This statement (or its
10.671  variations) are known as Scheffe lemma.
10.672
10.673  The formalization is more painful as one should jump back and forth between reals and ereals and justify
10.674 -all the time positivity or integrability (thankfully, measurability is handled more or less automatically).*}
10.675 +all the time positivity or integrability (thankfully, measurability is handled more or less automatically).\<close>
10.676
10.677  lemma Scheffe_lemma1:
10.678    assumes "\<And>n. integrable M (F n)" "integrable M f"

    11.1 --- a/src/HOL/Analysis/Tagged_Division.thy	Tue Jan 17 11:26:21 2017 +0100
11.2 +++ b/src/HOL/Analysis/Tagged_Division.thy	Tue Jan 17 13:59:10 2017 +0100
11.3 @@ -1312,7 +1312,7 @@
11.4  subsection \<open>Functions closed on boxes: morphisms from boxes to monoids\<close>
11.5
11.6  text \<open>This auxiliary structure is used to sum up over the elements of a division. Main theorem is
11.7 -  @{text operative_division}. Instances for the monoid are @{typ "'a option"}, @{typ real}, and
11.8 +  \<open>operative_division\<close>. Instances for the monoid are @{typ "'a option"}, @{typ real}, and
11.9    @{typ bool}.\<close>
11.10
11.11  paragraph \<open>Using additivity of lifted function to encode definedness.\<close>
11.12 @@ -2565,10 +2565,10 @@
11.13      have realff: "(real w) * 2^m < (real v) * 2^n \<longleftrightarrow> w * 2^m < v * 2^n" for m n v w
11.14        using of_nat_less_iff less_imp_of_nat_less by fastforce
11.15      have *: "\<forall>v w. ?K0(m,v) \<subseteq> ?K0(n,w) \<or> ?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
11.16 -      for m n --\<open>The symmetry argument requires a single HOL formula\<close>
11.17 +      for m n \<comment>\<open>The symmetry argument requires a single HOL formula\<close>
11.18      proof (rule linorder_wlog [where a=m and b=n], intro allI impI)
11.19        fix v w m and n::nat
11.20 -      assume "m \<le> n" --\<open>WLOG we can assume @{term"m \<le> n"}, when the first disjunct becomes impossible\<close>
11.21 +      assume "m \<le> n" \<comment>\<open>WLOG we can assume @{term"m \<le> n"}, when the first disjunct becomes impossible\<close>
11.22        have "?K0(n,w) \<subseteq> ?K0(m,v) \<or> interior(?K0(m,v)) \<inter> interior(?K0(n,w)) = {}"
11.23          apply (simp add: subset_box disjoint_interval)
11.24          apply (rule ccontr)

    12.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Jan 17 11:26:21 2017 +0100
12.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Jan 17 13:59:10 2017 +0100
12.3 @@ -499,9 +499,9 @@
12.4  proof -
12.5    obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto
12.6    define B1 where "B1 = {(LEAST x. x \<in> U)| U. U \<in> A}"
12.7 -  then have "countable B1" using countable A by (simp add: Setcompr_eq_image)
12.8 +  then have "countable B1" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
12.9    define B2 where "B2 = {(SOME x. x \<in> U)| U. U \<in> A}"
12.10 -  then have "countable B2" using countable A by (simp add: Setcompr_eq_image)
12.11 +  then have "countable B2" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
12.12    have "\<exists>b \<in> B1 \<union> B2. x < b \<and> b \<le> y" if "x < y" for x y
12.13    proof (cases)
12.14      assume "\<exists>z. x < z \<and> z < y"
12.15 @@ -509,27 +509,27 @@
12.16      define U where "U = {x<..<y}"
12.17      then have "open U" by simp
12.18      moreover have "z \<in> U" using z U_def by simp
12.19 -    ultimately obtain V where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF topological_basis A] by auto
12.20 +    ultimately obtain V where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
12.21      define w where "w = (SOME x. x \<in> V)"
12.22 -    then have "w \<in> V" using z \<in> V by (metis someI2)
12.23 -    then have "x < w \<and> w \<le> y" using w \<in> V V \<subseteq> U U_def by fastforce
12.24 -    moreover have "w \<in> B1 \<union> B2" using w_def B2_def V \<in> A by auto
12.25 +    then have "w \<in> V" using \<open>z \<in> V\<close> by (metis someI2)
12.26 +    then have "x < w \<and> w \<le> y" using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce
12.27 +    moreover have "w \<in> B1 \<union> B2" using w_def B2_def \<open>V \<in> A\<close> by auto
12.28      ultimately show ?thesis by auto
12.29    next
12.30      assume "\<not>(\<exists>z. x < z \<and> z < y)"
12.31      then have *: "\<And>z. z > x \<Longrightarrow> z \<ge> y" by auto
12.32      define U where "U = {x<..}"
12.33      then have "open U" by simp
12.34 -    moreover have "y \<in> U" using x < y U_def by simp
12.35 -    ultimately obtain "V" where "V \<in> A" "y \<in> V" "V \<subseteq> U" using topological_basisE[OF topological_basis A] by auto
12.36 -    have "U = {y..}" unfolding U_def using * x < y by auto
12.37 -    then have "V \<subseteq> {y..}" using V \<subseteq> U by simp
12.38 -    then have "(LEAST w. w \<in> V) = y" using y \<in> V by (meson Least_equality atLeast_iff subsetCE)
12.39 -    then have "y \<in> B1 \<union> B2" using V \<in> A B1_def by auto
12.40 -    moreover have "x < y \<and> y \<le> y" using x < y by simp
12.41 +    moreover have "y \<in> U" using \<open>x < y\<close> U_def by simp
12.42 +    ultimately obtain "V" where "V \<in> A" "y \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
12.43 +    have "U = {y..}" unfolding U_def using * \<open>x < y\<close> by auto
12.44 +    then have "V \<subseteq> {y..}" using \<open>V \<subseteq> U\<close> by simp
12.45 +    then have "(LEAST w. w \<in> V) = y" using \<open>y \<in> V\<close> by (meson Least_equality atLeast_iff subsetCE)
12.46 +    then have "y \<in> B1 \<union> B2" using \<open>V \<in> A\<close> B1_def by auto
12.47 +    moreover have "x < y \<and> y \<le> y" using \<open>x < y\<close> by simp
12.48      ultimately show ?thesis by auto
12.49    qed
12.50 -  moreover have "countable (B1 \<union> B2)" using countable B1 countable B2 by simp
12.51 +  moreover have "countable (B1 \<union> B2)" using \<open>countable B1\<close> \<open>countable B2\<close> by simp
12.52    ultimately show ?thesis by auto
12.53  qed
12.54
12.55 @@ -538,9 +538,9 @@
12.56  proof -
12.57    obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto
12.58    define B1 where "B1 = {(GREATEST x. x \<in> U) | U. U \<in> A}"
12.59 -  then have "countable B1" using countable A by (simp add: Setcompr_eq_image)
12.60 +  then have "countable B1" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
12.61    define B2 where "B2 = {(SOME x. x \<in> U)| U. U \<in> A}"
12.62 -  then have "countable B2" using countable A by (simp add: Setcompr_eq_image)
12.63 +  then have "countable B2" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
12.64    have "\<exists>b \<in> B1 \<union> B2. x \<le> b \<and> b < y" if "x < y" for x y
12.65    proof (cases)
12.66      assume "\<exists>z. x < z \<and> z < y"
12.67 @@ -548,27 +548,27 @@
12.68      define U where "U = {x<..<y}"
12.69      then have "open U" by simp
12.70      moreover have "z \<in> U" using z U_def by simp
12.71 -    ultimately obtain "V" where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF topological_basis A] by auto
12.72 +    ultimately obtain "V" where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
12.73      define w where "w = (SOME x. x \<in> V)"
12.74 -    then have "w \<in> V" using z \<in> V by (metis someI2)
12.75 -    then have "x \<le> w \<and> w < y" using w \<in> V V \<subseteq> U U_def by fastforce
12.76 -    moreover have "w \<in> B1 \<union> B2" using w_def B2_def V \<in> A by auto
12.77 +    then have "w \<in> V" using \<open>z \<in> V\<close> by (metis someI2)
12.78 +    then have "x \<le> w \<and> w < y" using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce
12.79 +    moreover have "w \<in> B1 \<union> B2" using w_def B2_def \<open>V \<in> A\<close> by auto
12.80      ultimately show ?thesis by auto
12.81    next
12.82      assume "\<not>(\<exists>z. x < z \<and> z < y)"
12.83      then have *: "\<And>z. z < y \<Longrightarrow> z \<le> x" using leI by blast
12.84      define U where "U = {..<y}"
12.85      then have "open U" by simp
12.86 -    moreover have "x \<in> U" using x < y U_def by simp
12.87 -    ultimately obtain "V" where "V \<in> A" "x \<in> V" "V \<subseteq> U" using topological_basisE[OF topological_basis A] by auto
12.88 -    have "U = {..x}" unfolding U_def using * x < y by auto
12.89 -    then have "V \<subseteq> {..x}" using V \<subseteq> U by simp
12.90 -    then have "(GREATEST x. x \<in> V) = x" using x \<in> V by (meson Greatest_equality atMost_iff subsetCE)
12.91 -    then have "x \<in> B1 \<union> B2" using V \<in> A B1_def by auto
12.92 -    moreover have "x \<le> x \<and> x < y" using x < y by simp
12.93 +    moreover have "x \<in> U" using \<open>x < y\<close> U_def by simp
12.94 +    ultimately obtain "V" where "V \<in> A" "x \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
12.95 +    have "U = {..x}" unfolding U_def using * \<open>x < y\<close> by auto
12.96 +    then have "V \<subseteq> {..x}" using \<open>V \<subseteq> U\<close> by simp
12.97 +    then have "(GREATEST x. x \<in> V) = x" using \<open>x \<in> V\<close> by (meson Greatest_equality atMost_iff subsetCE)
12.98 +    then have "x \<in> B1 \<union> B2" using \<open>V \<in> A\<close> B1_def by auto
12.99 +    moreover have "x \<le> x \<and> x < y" using \<open>x < y\<close> by simp
12.100      ultimately show ?thesis by auto
12.101    qed
12.102 -  moreover have "countable (B1 \<union> B2)" using countable B1 countable B2 by simp
12.103 +  moreover have "countable (B1 \<union> B2)" using \<open>countable B1\<close> \<open>countable B2\<close> by simp
12.104    ultimately show ?thesis by auto
12.105  qed
12.106
12.107 @@ -579,10 +579,10 @@
12.108      using countable_separating_set_linorder1 by auto
12.109    have "\<exists>b \<in> B. x < b \<and> b < y" if "x < y" for x y
12.110    proof -
12.111 -    obtain z where "x < z" "z < y" using x < y dense by blast
12.112 +    obtain z where "x < z" "z < y" using \<open>x < y\<close> dense by blast
12.113      then obtain b where "b \<in> B" "x < b \<and> b \<le> z" using B(2) by auto
12.114 -    then have "x < b \<and> b < y" using z < y by auto
12.115 -    then show ?thesis using b \<in> B by auto
12.116 +    then have "x < b \<and> b < y" using \<open>z < y\<close> by auto
12.117 +    then show ?thesis using \<open>b \<in> B\<close> by auto
12.118    qed
12.119    then show ?thesis using B(1) by auto
12.120  qed
12.121 @@ -680,7 +680,7 @@
12.122    shows "openin T (\<Inter>i \<in> I. U i)"
12.123  proof -
12.124    have "(\<Inter>i \<in> I. U i) \<subseteq> topspace T"
12.125 -    using I \<noteq> {} openin_subset[OF assms(3)] by auto
12.126 +    using \<open>I \<noteq> {}\<close> openin_subset[OF assms(3)] by auto
12.127    then show ?thesis
12.128      using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute)
12.129  qed

    13.1 --- a/src/HOL/Analysis/ex/Circle_Area.thy	Tue Jan 17 11:26:21 2017 +0100
13.2 +++ b/src/HOL/Analysis/ex/Circle_Area.thy	Tue Jan 17 13:59:10 2017 +0100
13.3 @@ -4,7 +4,7 @@
13.4  A proof that the area of a circle with radius R is R\<^sup>2\<pi>.
13.5  *)
13.6
13.7 -section {* The area of a circle *}
13.8 +section \<open>The area of a circle\<close>
13.9
13.10  theory Circle_Area
13.11  imports Complex_Main Interval_Integral
13.12 @@ -157,13 +157,13 @@
13.13    also have "... = \<integral>\<^sup>+x. R * \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel"
13.14    proof (rule nn_integral_cong)
13.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"
13.16 -      by (subst nn_integral_real_affine[OF _ R \<noteq> 0, of _ 0]) simp_all
13.17 +      by (subst nn_integral_real_affine[OF _ \<open>R \<noteq> 0\<close>, of _ 0]) simp_all
13.18    qed
13.19    also have "... = R * \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel"
13.20      using R by (intro nn_integral_cmult) simp_all
13.21    also from R have "(\<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (x,R*y) \<partial>lborel \<partial>lborel) =
13.22                          R * \<integral>\<^sup>+x. \<integral>\<^sup>+y. indicator ?A (R*x,R*y) \<partial>lborel \<partial>lborel"
13.23 -    by (subst nn_integral_real_affine[OF _ R \<noteq> 0, of _ 0]) simp_all
13.24 +    by (subst nn_integral_real_affine[OF _ \<open>R \<noteq> 0\<close>, of _ 0]) simp_all
13.25    also {
13.26      fix x y
13.27      have A: "(R*x, R*y) = R *\<^sub>R (x,y)" by simp

    14.1 --- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Tue Jan 17 11:26:21 2017 +0100
14.2 +++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Tue Jan 17 13:59:10 2017 +0100
14.3 @@ -268,7 +268,7 @@
14.4
14.5  context bourbaki_witt_fixpoint begin
14.6
14.7 -lemma in_Chains_finite: -- \<open>Translation from @{thm in_chain_finite}.\<close>
14.8 +lemma in_Chains_finite: \<comment> \<open>Translation from @{thm in_chain_finite}.\<close>
14.9    assumes "M \<in> Chains leq"
14.10    and "M \<noteq> {}"
14.11    and "finite M"

    15.1 --- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Tue Jan 17 11:26:21 2017 +0100
15.2 +++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Tue Jan 17 13:59:10 2017 +0100
15.3 @@ -773,8 +773,8 @@
15.4    shows "\<exists>x\<in>s. alw (ev (HLD {x})) \<omega>"
15.5  proof -
15.6    have "\<forall>i\<in>UNIV. \<exists>x\<in>s. \<omega> !! i = x"
15.7 -    using alw (HLD s) \<omega> by (simp add: alw_iff_sdrop HLD_iff)
15.8 -  from pigeonhole_infinite_rel[OF infinite_UNIV_nat finite s this]
15.9 +    using \<open>alw (HLD s) \<omega>\<close> by (simp add: alw_iff_sdrop HLD_iff)
15.10 +  from pigeonhole_infinite_rel[OF infinite_UNIV_nat \<open>finite s\<close> this]
15.11    show ?thesis
15.12      by (simp add: HLD_iff infinite_iff_alw_ev[symmetric])
15.13  qed

    16.1 --- a/src/HOL/Library/Multiset.thy	Tue Jan 17 11:26:21 2017 +0100
16.2 +++ b/src/HOL/Library/Multiset.thy	Tue Jan 17 13:59:10 2017 +0100
16.3 @@ -2805,7 +2805,7 @@
16.4      case (add z Z)
16.5      obtain X' Y' Z' where *: "add_mset z X + Z = Z' + X'" "add_mset z Y + Z = Z' + Y'" "Y' \<noteq> {#}"
16.6        "\<forall>x \<in> set_mset X'. \<exists>y \<in> set_mset Y'. (x, y) \<in> s"
16.7 -      using mult_implies_one_step[OF trans s add(2)] by auto
16.8 +      using mult_implies_one_step[OF \<open>trans s\<close> add(2)] by auto
16.9      consider Z2 where "Z' = add_mset z Z2" | X2 Y2 where "X' = add_mset z X2" "Y' = add_mset z Y2"
16.10        using *(1,2) by (metis add_mset_remove_trivial_If insert_iff set_mset_add_mset_insert union_iff)
16.11      thus ?case
16.12 @@ -2813,9 +2813,9 @@
16.13        case 1 thus ?thesis using * one_step_implies_mult[of Y' X' s Z2]
16.14          by (auto simp: add.commute[of _ "{#_#}"] add.assoc intro: add(1))
16.15      next
16.16 -      case 2 then obtain y where "y \<in> set_mset Y2" "(z, y) \<in> s" using *(4) irrefl s
16.17 +      case 2 then obtain y where "y \<in> set_mset Y2" "(z, y) \<in> s" using *(4) \<open>irrefl s\<close>
16.18          by (auto simp: irrefl_def)
16.19 -      moreover from this transD[OF trans s _ this(2)]
16.20 +      moreover from this transD[OF \<open>trans s\<close> _ this(2)]
16.21        have "x' \<in> set_mset X2 \<Longrightarrow> \<exists>y \<in> set_mset Y2. (x', y) \<in> s" for x'
16.22          using 2 *(4)[rule_format, of x'] by auto
16.23        ultimately show ?thesis using  * one_step_implies_mult[of Y2 X2 s Z'] 2
16.24 @@ -2825,7 +2825,7 @@
16.25  next
16.26    assume ?R then obtain I J K
16.27      where "Y = I + J" "X = I + K" "J \<noteq> {#}" "\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> s"
16.28 -    using mult_implies_one_step[OF trans s] by blast
16.29 +    using mult_implies_one_step[OF \<open>trans s\<close>] by blast
16.30    thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps)
16.31  qed
16.32
16.33 @@ -2887,7 +2887,7 @@
16.34  proof -
16.35    { assume "N \<noteq> M" "M - M \<inter># N = {#}"
16.36      then obtain y where "count N y \<noteq> count M y" by (auto simp: count_inject[symmetric])
16.37 -    then have "\<exists>y. count M y < count N y" using M - M \<inter># N = {#}
16.38 +    then have "\<exists>y. count M y < count N y" using \<open>M - M \<inter># N = {#}\<close>
16.39        by (auto simp: count_inject[symmetric] dest!: le_neq_implies_less fun_cong[of _ _ y])
16.40    }
16.41    then have "multeqp P N M \<longleftrightarrow> multp P N M \<or> N = M"

    17.1 --- a/src/HOL/Library/Perm.thy	Tue Jan 17 11:26:21 2017 +0100
17.2 +++ b/src/HOL/Library/Perm.thy	Tue Jan 17 13:59:10 2017 +0100
17.3 @@ -12,7 +12,7 @@
17.4    Grieviously missing are cycles since these would require more
17.5    elaboration, e.g. the concept of distinct lists equivalent
17.6    under rotation, which maybe would also deserve its own theory.
17.7 -  But see theory @{text "src/HOL/ex/Perm_Fragments.thy"} for
17.8 +  But see theory \<open>src/HOL/ex/Perm_Fragments.thy\<close> for
17.9    fragments on that.
17.10  \<close>
17.11

    18.1 --- a/src/HOL/Library/Polynomial_FPS.thy	Tue Jan 17 11:26:21 2017 +0100
18.2 +++ b/src/HOL/Library/Polynomial_FPS.thy	Tue Jan 17 13:59:10 2017 +0100
18.3 @@ -163,7 +163,7 @@
18.4    The following simproc can reduce the equality of two polynomial FPSs two equality of the
18.5    respective polynomials. A polynomial FPS is one that only has finitely many non-zero
18.6    coefficients and can therefore be written as @{term "fps_of_poly p"} for some
18.7 -  polynomial @{text "p"}.
18.8 +  polynomial \<open>p\<close>.
18.9
18.10    This may sound trivial, but it covers a number of annoying side conditions like
18.11    @{term "1 + X \<noteq> 0"} that would otherwise not be solved automatically.

    19.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Tue Jan 17 11:26:21 2017 +0100
19.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Tue Jan 17 13:59:10 2017 +0100
19.3 @@ -52,7 +52,7 @@
19.4  subsection \<open>Lifting elements into the field of fractions\<close>
19.5
19.6  definition to_fract :: "'a :: idom \<Rightarrow> 'a fract" where "to_fract x = Fract x 1"
19.7 -  -- \<open>FIXME: name \<open>of_idom\<close>, abbreviation\<close>
19.8 +  \<comment> \<open>FIXME: name \<open>of_idom\<close>, abbreviation\<close>
19.9
19.10  lemma to_fract_0 [simp]: "to_fract 0 = 0"
19.11    by (simp add: to_fract_def eq_fract Zero_fract_def)

    20.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Tue Jan 17 11:26:21 2017 +0100
20.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Tue Jan 17 13:59:10 2017 +0100
20.3 @@ -187,7 +187,7 @@
20.4  proof -
20.5    show "class.factorial_semiring divide plus minus zero times one
20.6       unit_factor normalize"
20.7 -  proof (standard, rule factorial_semiring_altI_aux) -- \<open>FIXME rule\<close>
20.8 +  proof (standard, rule factorial_semiring_altI_aux) \<comment> \<open>FIXME rule\<close>
20.9      fix x assume "x \<noteq> 0"
20.10      thus "finite {p. p dvd x \<and> normalize p = p}"
20.11      proof (induction "euclidean_size x" arbitrary: x rule: less_induct)

    21.1 --- a/src/HOL/Number_Theory/Primes.thy	Tue Jan 17 11:26:21 2017 +0100
21.2 +++ b/src/HOL/Number_Theory/Primes.thy	Tue Jan 17 13:59:10 2017 +0100
21.3 @@ -310,7 +310,7 @@
21.4    "prime (numeral m :: nat) \<longleftrightarrow>
21.5      (1::nat) < numeral m \<and>
21.6      (\<forall>n::nat\<in>set [2..<numeral m]. \<not> n dvd numeral m)"
21.7 -  by (fact prime_nat_simp) -- \<open>TODO Sieve Of Erathosthenes might speed this up\<close>
21.8 +  by (fact prime_nat_simp) \<comment> \<open>TODO Sieve Of Erathosthenes might speed this up\<close>
21.9
21.10
21.11  text\<open>A bit of regression testing:\<close>

    22.1 --- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Tue Jan 17 11:26:21 2017 +0100
22.2 +++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Tue Jan 17 13:59:10 2017 +0100
22.3 @@ -4,7 +4,7 @@
22.4  imports Gauss
22.5  begin
22.6
22.7 -text {* The proof is based on Gauss's fifth proof, which can be found at http://www.lehigh.edu/~shw2/q-recip/gauss5.pdf *}
22.8 +text \<open>The proof is based on Gauss's fifth proof, which can be found at http://www.lehigh.edu/~shw2/q-recip/gauss5.pdf\<close>
22.9
22.10  locale QR =
22.11    fixes p :: "nat"