removed dots at the end of (sub)titles
authornipkow
Mon Apr 09 16:20:23 2018 +0200 (13 months ago)
changeset 67968a5ad4c015d1c
parent 67967 5a4280946a25
child 67971 e9f66b35d636
removed dots at the end of (sub)titles
src/HOL/Analysis/Arcwise_Connected.thy
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Conformal_Mappings.thy
src/HOL/Analysis/Connected.thy
src/HOL/Analysis/Continuous_Extension.thy
src/HOL/Analysis/Continuum_Not_Denumerable.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Derivative.thy
src/HOL/Analysis/Determinants.thy
src/HOL/Analysis/Fashoda_Theorem.thy
src/HOL/Analysis/Finite_Cartesian_Product.thy
src/HOL/Analysis/Further_Topology.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Jordan_Curve.thy
src/HOL/Analysis/Lebesgue_Measure.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Poly_Roots.thy
src/HOL/Analysis/Polytope.thy
src/HOL/Analysis/Riemann_Mapping.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Analysis/Tagged_Division.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Analysis/Arcwise_Connected.thy	Sun Apr 08 12:31:08 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Arcwise_Connected.thy	Mon Apr 09 16:20:23 2018 +0200
     1.3 @@ -109,7 +109,7 @@
     1.4  
     1.5  subsection\<open>Arcwise Connections\<close>
     1.6  
     1.7 -subsection\<open>Density of points with dyadic rational coordinates.\<close>
     1.8 +subsection\<open>Density of points with dyadic rational coordinates\<close>
     1.9  
    1.10  proposition closure_dyadic_rationals:
    1.11      "closure (\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>.
     2.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Apr 08 12:31:08 2018 +0200
     2.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Mon Apr 09 16:20:23 2018 +0200
     2.3 @@ -16,7 +16,7 @@
     2.4  (*              (c) Copyright, John Harrison 1998-2008                       *)
     2.5  (* ========================================================================= *)
     2.6  
     2.7 -section \<open>Results connected with topological dimension.\<close>
     2.8 +section \<open>Results connected with topological dimension\<close>
     2.9  
    2.10  theory Brouwer_Fixpoint
    2.11  imports Path_Connected Homeomorphism
    2.12 @@ -117,7 +117,7 @@
    2.13  qed
    2.14  
    2.15  
    2.16 -subsection \<open>The key "counting" observation, somewhat abstracted.\<close>
    2.17 +subsection \<open>The key "counting" observation, somewhat abstracted\<close>
    2.18  
    2.19  lemma kuhn_counting_lemma:
    2.20    fixes bnd compo compo' face S F
    2.21 @@ -148,7 +148,7 @@
    2.22      by auto
    2.23  qed
    2.24  
    2.25 -subsection \<open>The odd/even result for faces of complete vertices, generalized.\<close>
    2.26 +subsection \<open>The odd/even result for faces of complete vertices, generalized\<close>
    2.27  
    2.28  lemma kuhn_complete_lemma:
    2.29    assumes [simp]: "finite simplices"
    2.30 @@ -2367,7 +2367,7 @@
    2.31  qed
    2.32  
    2.33  
    2.34 -subsection\<open>Punctured affine hulls, etc.\<close>
    2.35 +subsection\<open>Punctured affine hulls, etc\<close>
    2.36  
    2.37  lemma continuous_on_compact_surface_projection_aux:
    2.38    fixes S :: "'a::t2_space set"
    2.39 @@ -2716,7 +2716,7 @@
    2.40      by blast
    2.41  qed
    2.42  
    2.43 -subsection\<open>Absolute retracts, Etc.\<close>
    2.44 +subsection\<open>Absolute retracts, etc\<close>
    2.45  
    2.46  text\<open>Absolute retracts (AR), absolute neighbourhood retracts (ANR) and also
    2.47   Euclidean neighbourhood retracts (ENR). We define AR and ANR by
    2.48 @@ -3110,7 +3110,7 @@
    2.49    shows "S homeomorphic T \<Longrightarrow> ANR S \<longleftrightarrow> ANR T"
    2.50  by (metis ANR_homeomorphic_ANR homeomorphic_sym)
    2.51  
    2.52 -subsection\<open> Analogous properties of ENRs.\<close>
    2.53 +subsection\<open> Analogous properties of ENRs\<close>
    2.54  
    2.55  proposition ENR_imp_absolute_neighbourhood_retract:
    2.56    fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
    2.57 @@ -4274,7 +4274,7 @@
    2.58    shows "ANR c"
    2.59    by (metis ANR_connected_component_ANR assms componentsE)
    2.60  
    2.61 -subsection\<open>Original ANR material, now for ENRs.\<close>
    2.62 +subsection\<open>Original ANR material, now for ENRs\<close>
    2.63  
    2.64  lemma ENR_bounded:
    2.65    fixes S :: "'a::euclidean_space set"
    2.66 @@ -4438,7 +4438,7 @@
    2.67    by (simp add: ENR_imp_ANR ENR_sphere)
    2.68  
    2.69  
    2.70 -subsection\<open>Spheres are connected, etc.\<close>
    2.71 +subsection\<open>Spheres are connected, etc\<close>
    2.72  
    2.73  lemma locally_path_connected_sphere_gen:
    2.74    fixes S :: "'a::euclidean_space set"
     3.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Apr 08 12:31:08 2018 +0200
     3.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Apr 09 16:20:23 2018 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space.\<close>
     3.5 +section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space\<close>
     3.6  
     3.7  theory Cartesian_Euclidean_Space
     3.8  imports Finite_Cartesian_Product Derivative
     3.9 @@ -21,7 +21,7 @@
    3.10    qed simp
    3.11  qed simp
    3.12  
    3.13 -subsection\<open>Basic componentwise operations on vectors.\<close>
    3.14 +subsection\<open>Basic componentwise operations on vectors\<close>
    3.15  
    3.16  instantiation vec :: (times, finite) times
    3.17  begin
    3.18 @@ -93,7 +93,7 @@
    3.19    where "c *s x = (\<chi> i. c * (x$i))"
    3.20  
    3.21  
    3.22 -subsection \<open>A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space.\<close>
    3.23 +subsection \<open>A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space\<close>
    3.24  
    3.25  lemma sum_cong_aux:
    3.26    "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> sum f A = sum g A"
    3.27 @@ -170,7 +170,7 @@
    3.28    vector_scaleR_component cond_component
    3.29  
    3.30  
    3.31 -subsection \<open>Some frequently useful arithmetic lemmas over vectors.\<close>
    3.32 +subsection \<open>Some frequently useful arithmetic lemmas over vectors\<close>
    3.33  
    3.34  instance vec :: (semigroup_mult, finite) semigroup_mult
    3.35    by standard (vector mult.assoc)
    3.36 @@ -719,7 +719,7 @@
    3.37    done
    3.38  
    3.39  
    3.40 -subsection\<open>Some bounds on components etc. relative to operator norm.\<close>
    3.41 +subsection\<open>Some bounds on components etc. relative to operator norm\<close>
    3.42  
    3.43  lemma norm_column_le_onorm:
    3.44    fixes A :: "real^'n^'m"
    3.45 @@ -1416,7 +1416,7 @@
    3.46  
    3.47  
    3.48  subsection \<open>Component of the differential must be zero if it exists at a local
    3.49 -  maximum or minimum for that corresponding component.\<close>
    3.50 +  maximum or minimum for that corresponding component\<close>
    3.51  
    3.52  lemma differential_zero_maxmin_cart:
    3.53    fixes f::"real^'a \<Rightarrow> real^'b"
    3.54 @@ -1489,7 +1489,7 @@
    3.55  
    3.56  end
    3.57  
    3.58 -subsection\<open>The collapse of the general concepts to dimension one.\<close>
    3.59 +subsection\<open>The collapse of the general concepts to dimension one\<close>
    3.60  
    3.61  lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
    3.62    by (simp add: vec_eq_iff)
    3.63 @@ -1510,7 +1510,7 @@
    3.64    by (auto simp add: norm_real dist_norm)
    3.65  
    3.66  
    3.67 -subsection\<open>Explicit vector construction from lists.\<close>
    3.68 +subsection\<open>Explicit vector construction from lists\<close>
    3.69  
    3.70  definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)"
    3.71  
     4.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun Apr 08 12:31:08 2018 +0200
     4.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Apr 09 16:20:23 2018 +0200
     4.3 @@ -3550,7 +3550,7 @@
     4.4    apply (force simp: algebra_simps)
     4.5    done
     4.6  
     4.7 -subsubsection\<open>Some lemmas about negating a path.\<close>
     4.8 +subsubsection\<open>Some lemmas about negating a path\<close>
     4.9  
    4.10  lemma valid_path_negatepath: "valid_path \<gamma> \<Longrightarrow> valid_path (uminus \<circ> \<gamma>)"
    4.11     unfolding o_def using piecewise_C1_differentiable_neg valid_path_def by blast
    4.12 @@ -3965,7 +3965,7 @@
    4.13  qed
    4.14  
    4.15  
    4.16 -subsection\<open>Continuity of winding number and invariance on connected sets.\<close>
    4.17 +subsection\<open>Continuity of winding number and invariance on connected sets\<close>
    4.18  
    4.19  lemma continuous_at_winding_number:
    4.20    fixes z::complex
    4.21 @@ -4436,7 +4436,7 @@
    4.22  qed
    4.23  
    4.24  
    4.25 -subsection\<open>Cauchy's integral formula, again for a convex enclosing set.\<close>
    4.26 +subsection\<open>Cauchy's integral formula, again for a convex enclosing set\<close>
    4.27  
    4.28  lemma Cauchy_integral_formula_weak:
    4.29      assumes s: "convex s" and "finite k" and conf: "continuous_on s f"
    4.30 @@ -5374,7 +5374,7 @@
    4.31    using assms by (auto simp: vector_derivative_circlepath norm_mult intro!: contour_integral_uniform_limit)
    4.32  
    4.33  
    4.34 -subsection\<open> General stepping result for derivative formulas.\<close>
    4.35 +subsection\<open> General stepping result for derivative formulas\<close>
    4.36  
    4.37  proposition Cauchy_next_derivative:
    4.38    assumes "continuous_on (path_image \<gamma>) f'"
    4.39 @@ -5614,7 +5614,7 @@
    4.40      by simp (rule fder)
    4.41  qed
    4.42  
    4.43 -subsection\<open> Existence of all higher derivatives.\<close>
    4.44 +subsection\<open>Existence of all higher derivatives\<close>
    4.45  
    4.46  proposition derivative_is_holomorphic:
    4.47    assumes "open s"
    4.48 @@ -5699,7 +5699,7 @@
    4.49  qed
    4.50  
    4.51  
    4.52 -subsection\<open> Morera's theorem.\<close>
    4.53 +subsection\<open>Morera's theorem\<close>
    4.54  
    4.55  lemma Morera_local_triangle_ball:
    4.56    assumes "\<And>z. z \<in> s
    4.57 @@ -5783,7 +5783,7 @@
    4.58  
    4.59  
    4.60  
    4.61 -subsection\<open> Combining theorems for higher derivatives including Leibniz rule.\<close>
    4.62 +subsection\<open>Combining theorems for higher derivatives including Leibniz rule\<close>
    4.63  
    4.64  lemma higher_deriv_linear [simp]:
    4.65      "(deriv ^^ n) (\<lambda>w. c*w) = (\<lambda>z. if n = 0 then c*z else if n = 1 then c else 0)"
    4.66 @@ -6139,7 +6139,7 @@
    4.67    by (simp add: power2_eq_square)
    4.68  
    4.69  
    4.70 -subsection\<open>A holomorphic function is analytic, i.e. has local power series.\<close>
    4.71 +subsection\<open>A holomorphic function is analytic, i.e. has local power series\<close>
    4.72  
    4.73  theorem holomorphic_power_series:
    4.74    assumes holf: "f holomorphic_on ball z r"
    4.75 @@ -6255,7 +6255,7 @@
    4.76  qed
    4.77  
    4.78  
    4.79 -subsection\<open>The Liouville theorem and the Fundamental Theorem of Algebra.\<close>
    4.80 +subsection\<open>The Liouville theorem and the Fundamental Theorem of Algebra\<close>
    4.81  
    4.82  text\<open> These weak Liouville versions don't even need the derivative formula.\<close>
    4.83  
    4.84 @@ -6343,7 +6343,7 @@
    4.85  qed
    4.86  
    4.87  
    4.88 -subsection\<open> Weierstrass convergence theorem.\<close>
    4.89 +subsection\<open>Weierstrass convergence theorem\<close>
    4.90  
    4.91  proposition holomorphic_uniform_limit:
    4.92    assumes cont: "eventually (\<lambda>n. continuous_on (cball z r) (f n) \<and> (f n) holomorphic_on ball z r) F"
    4.93 @@ -6490,7 +6490,7 @@
    4.94  qed
    4.95  
    4.96  
    4.97 -subsection\<open>Some more simple/convenient versions for applications.\<close>
    4.98 +subsection\<open>Some more simple/convenient versions for applications\<close>
    4.99  
   4.100  lemma holomorphic_uniform_sequence:
   4.101    assumes S: "open S"
   4.102 @@ -6548,7 +6548,7 @@
   4.103  qed
   4.104  
   4.105  
   4.106 -subsection\<open>On analytic functions defined by a series.\<close>
   4.107 +subsection\<open>On analytic functions defined by a series\<close>
   4.108   
   4.109  lemma series_and_derivative_comparison:
   4.110    fixes S :: "complex set"
   4.111 @@ -6767,7 +6767,7 @@
   4.112    by (simp add: analytic_on_open holomorphic_iff_power_series)
   4.113  
   4.114  
   4.115 -subsection\<open>Equality between holomorphic functions, on open ball then connected set.\<close>
   4.116 +subsection\<open>Equality between holomorphic functions, on open ball then connected set\<close>
   4.117  
   4.118  lemma holomorphic_fun_eq_on_ball:
   4.119     "\<lbrakk>f holomorphic_on ball z r; g holomorphic_on ball z r;
   4.120 @@ -6846,7 +6846,7 @@
   4.121    done
   4.122  
   4.123  
   4.124 -subsection\<open>Some basic lemmas about poles/singularities.\<close>
   4.125 +subsection\<open>Some basic lemmas about poles/singularities\<close>
   4.126  
   4.127  lemma pole_lemma:
   4.128    assumes holf: "f holomorphic_on s" and a: "a \<in> interior s"
   4.129 @@ -7002,7 +7002,7 @@
   4.130  qed
   4.131  
   4.132  
   4.133 -subsection\<open>General, homology form of Cauchy's theorem.\<close>
   4.134 +subsection\<open>General, homology form of Cauchy's theorem\<close>
   4.135  
   4.136  text\<open>Proof is based on Dixon's, as presented in Lang's "Complex Analysis" book (page 147).\<close>
   4.137  
     5.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Apr 08 12:31:08 2018 +0200
     5.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Apr 09 16:20:23 2018 +0200
     5.3 @@ -174,7 +174,7 @@
     5.4    "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a"
     5.5    by (metis DERIV_zero_unique UNIV_I convex_UNIV)
     5.6  
     5.7 -subsection \<open>Some limit theorems about real part of real series etc.\<close>
     5.8 +subsection \<open>Some limit theorems about real part of real series etc\<close>
     5.9  
    5.10  (*MOVE? But not to Finite_Cartesian_Product*)
    5.11  lemma sums_vec_nth :
     6.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Apr 08 12:31:08 2018 +0200
     6.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Apr 09 16:20:23 2018 +0200
     6.3 @@ -77,7 +77,7 @@
     6.4    "f holomorphic_on s \<Longrightarrow> (\<lambda>x. exp (f x)) holomorphic_on s"
     6.5    using holomorphic_on_compose[OF _ holomorphic_on_exp] by (simp add: o_def)
     6.6  
     6.7 -subsection\<open>Euler and de Moivre formulas.\<close>
     6.8 +subsection\<open>Euler and de Moivre formulas\<close>
     6.9  
    6.10  text\<open>The sine series times @{term i}\<close>
    6.11  lemma sin_i_eq: "(\<lambda>n. (\<i> * sin_coeff n) * z^n) sums (\<i> * sin z)"
    6.12 @@ -176,7 +176,7 @@
    6.13  lemma holomorphic_on_cos: "cos holomorphic_on s"
    6.14    by (simp add: field_differentiable_within_cos holomorphic_on_def)
    6.15  
    6.16 -subsection\<open>Get a nice real/imaginary separation in Euler's formula.\<close>
    6.17 +subsection\<open>Get a nice real/imaginary separation in Euler's formula\<close>
    6.18  
    6.19  lemma Euler: "exp(z) = of_real(exp(Re z)) *
    6.20                (of_real(cos(Im z)) + \<i> * of_real(sin(Im z)))"
    6.21 @@ -626,7 +626,7 @@
    6.22  qed
    6.23  
    6.24  
    6.25 -subsection\<open>Taylor series for complex exponential, sine and cosine.\<close>
    6.26 +subsection\<open>Taylor series for complex exponential, sine and cosine\<close>
    6.27  
    6.28  declare power_Suc [simp del]
    6.29  
    6.30 @@ -3503,7 +3503,7 @@
    6.31  lemma of_real_arccos: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
    6.32    by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0)
    6.33  
    6.34 -subsection\<open>Some interrelationships among the real inverse trig functions.\<close>
    6.35 +subsection\<open>Some interrelationships among the real inverse trig functions\<close>
    6.36  
    6.37  lemma arccos_arctan:
    6.38    assumes "-1 < x" "x < 1"
    6.39 @@ -3573,7 +3573,7 @@
    6.40    using arccos_arcsin_sqrt_pos [of "-x"]
    6.41    by (simp add: arccos_minus)
    6.42  
    6.43 -subsection\<open>continuity results for arcsin and arccos.\<close>
    6.44 +subsection\<open>Continuity results for arcsin and arccos\<close>
    6.45  
    6.46  lemma continuous_on_Arcsin_real [continuous_intros]:
    6.47      "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arcsin"
     7.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Sun Apr 08 12:31:08 2018 +0200
     7.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Mon Apr 09 16:20:23 2018 +0200
     7.3 @@ -1,4 +1,4 @@
     7.4 -section \<open>Conformal Mappings. Consequences of Cauchy's integral theorem.\<close>
     7.5 +section \<open>Conformal Mappings and Consequences of Cauchy's integral theorem\<close>
     7.6  
     7.7  text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2016)\<close>
     7.8  
     8.1 --- a/src/HOL/Analysis/Connected.thy	Sun Apr 08 12:31:08 2018 +0200
     8.2 +++ b/src/HOL/Analysis/Connected.thy	Mon Apr 09 16:20:23 2018 +0200
     8.3 @@ -2,13 +2,13 @@
     8.4      Material split off from Topology_Euclidean_Space
     8.5  *)
     8.6  
     8.7 -section \<open>Connected Components, Homeomorphisms, Baire property, etc.\<close>
     8.8 +section \<open>Connected Components, Homeomorphisms, Baire property, etc\<close>
     8.9  
    8.10  theory Connected
    8.11  imports Topology_Euclidean_Space
    8.12  begin
    8.13  
    8.14 -subsection%unimportant \<open>More properties of closed balls, spheres, etc.\<close>
    8.15 +subsection%unimportant \<open>More properties of closed balls, spheres, etc\<close>
    8.16  
    8.17  lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
    8.18    apply (simp add: interior_def, safe)
    8.19 @@ -961,7 +961,7 @@
    8.20    qed
    8.21  qed
    8.22  
    8.23 -subsection%unimportant \<open>Some theorems on sups and infs using the notion "bounded".\<close>
    8.24 +subsection%unimportant \<open>Some theorems on sups and infs using the notion "bounded"\<close>
    8.25  
    8.26  lemma bounded_real: "bounded (S::real set) \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. \<bar>x\<bar> \<le> a)"
    8.27    by (simp add: bounded_iff)
    8.28 @@ -1139,7 +1139,7 @@
    8.29  qed
    8.30  
    8.31  
    8.32 -subsection%unimportant\<open>Relations among convergence and absolute convergence for power series.\<close>
    8.33 +subsection%unimportant\<open>Relations among convergence and absolute convergence for power series\<close>
    8.34  
    8.35  lemma summable_imp_bounded:
    8.36    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
    8.37 @@ -1515,7 +1515,7 @@
    8.38      by (simp add: compact_eq_bounded_closed)
    8.39  qed
    8.40  
    8.41 -subsection%unimportant \<open>Equality of continuous functions on closure and related results.\<close>
    8.42 +subsection%unimportant \<open>Equality of continuous functions on closure and related results\<close>
    8.43  
    8.44  lemma continuous_closedin_preimage_constant:
    8.45    fixes f :: "_ \<Rightarrow> 'b::t1_space"
    8.46 @@ -2047,7 +2047,7 @@
    8.47    shows "bounded(f ` S)"
    8.48    by (metis (no_types, lifting) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure)
    8.49  
    8.50 -subsection%unimportant \<open>Making a continuous function avoid some value in a neighbourhood.\<close>
    8.51 +subsection%unimportant \<open>Making a continuous function avoid some value in a neighbourhood\<close>
    8.52  
    8.53  lemma continuous_within_avoid:
    8.54    fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
    8.55 @@ -2363,7 +2363,7 @@
    8.56      unfolding mem_interior using \<open>e > 0\<close> by auto
    8.57  qed
    8.58  
    8.59 -subsection \<open>Continuity implies uniform continuity on a compact domain.\<close>
    8.60 +subsection \<open>Continuity implies uniform continuity on a compact domain\<close>
    8.61  
    8.62  text\<open>From the proof of the Heine-Borel theorem: Lemma 2 in section 3.7, page 69 of
    8.63  J. C. Burkill and H. Burkill. A Second Course in Mathematical Analysis (CUP, 2002)\<close>
    8.64 @@ -2666,7 +2666,7 @@
    8.65  qed
    8.66  
    8.67  
    8.68 -subsection \<open>The diameter of a set.\<close>
    8.69 +subsection \<open>The diameter of a set\<close>
    8.70  
    8.71  definition%important diameter :: "'a::metric_space set \<Rightarrow> real" where
    8.72    "diameter S = (if S = {} then 0 else SUP (x,y):S\<times>S. dist x y)"
    8.73 @@ -3014,7 +3014,7 @@
    8.74  qed
    8.75  
    8.76  
    8.77 -subsection%unimportant \<open>Compact sets and the closure operation.\<close>
    8.78 +subsection%unimportant \<open>Compact sets and the closure operation\<close>
    8.79  
    8.80  lemma closed_scaling:
    8.81    fixes S :: "'a::real_normed_vector set"
    8.82 @@ -3321,7 +3321,7 @@
    8.83  using assms
    8.84  by (auto simp: continuous_on_id intro: continuous_on_cases_le [where h = id, simplified])
    8.85  
    8.86 -subsubsection\<open>Some more convenient intermediate-value theorem formulations.\<close>
    8.87 +subsubsection\<open>Some more convenient intermediate-value theorem formulations\<close>
    8.88  
    8.89  lemma connected_ivt_hyperplane:
    8.90    assumes "connected S" and xy: "x \<in> S" "y \<in> S" and b: "inner a x \<le> b" "b \<le> inner a y"
    8.91 @@ -3901,7 +3901,7 @@
    8.92  qed
    8.93  
    8.94  
    8.95 -subsection \<open>"Isometry" (up to constant bounds) of injective linear map etc.\<close>
    8.96 +subsection \<open>"Isometry" (up to constant bounds) of injective linear map etc\<close>
    8.97  
    8.98  lemma cauchy_isometric:
    8.99    assumes e: "e > 0"
   8.100 @@ -4976,7 +4976,7 @@
   8.101  
   8.102  
   8.103  
   8.104 -subsection\<open>A couple of lemmas about components (see Newman IV, 3.3 and 3.4).\<close>
   8.105 +subsection\<open>A couple of lemmas about components (see Newman IV, 3.3 and 3.4)\<close>
   8.106  
   8.107  
   8.108  lemma connected_Un_clopen_in_complement:
     9.1 --- a/src/HOL/Analysis/Continuous_Extension.thy	Sun Apr 08 12:31:08 2018 +0200
     9.2 +++ b/src/HOL/Analysis/Continuous_Extension.thy	Mon Apr 09 16:20:23 2018 +0200
     9.3 @@ -295,7 +295,7 @@
     9.4  using%unimportant assms by (auto intro: Urysohn_local [of UNIV S T a b])
     9.5  
     9.6  
     9.7 -subsection\<open> The Dugundji extension theorem, and Tietze variants as corollaries.\<close>
     9.8 +subsection\<open>The Dugundji extension theorem and Tietze variants as corollaries\<close>
     9.9  
    9.10  text%important\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
    9.11  http://projecteuclid.org/euclid.pjm/1103052106\<close>
    10.1 --- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Sun Apr 08 12:31:08 2018 +0200
    10.2 +++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Mon Apr 09 16:20:23 2018 +0200
    10.3 @@ -3,7 +3,7 @@
    10.4      Author:     Johannes Hölzl, TU München
    10.5  *)
    10.6  
    10.7 -section \<open>Non-denumerability of the Continuum.\<close>
    10.8 +section \<open>Non-denumerability of the Continuum\<close>
    10.9  
   10.10  theory Continuum_Not_Denumerable
   10.11  imports
    11.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Apr 08 12:31:08 2018 +0200
    11.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Apr 09 16:20:23 2018 +0200
    11.3 @@ -4283,7 +4283,7 @@
    11.4  by (metis low_dim_interior)
    11.5  
    11.6  
    11.7 -subsection \<open>Caratheodory's theorem.\<close>
    11.8 +subsection \<open>Caratheodory's theorem\<close>
    11.9  
   11.10  lemma convex_hull_caratheodory_aff_dim:
   11.11    fixes p :: "('a::euclidean_space) set"
   11.12 @@ -5151,7 +5151,7 @@
   11.13    by (metis Int_absorb1 Int_absorb2 convex_hull_subset_affine_hull hull_hull hull_mono hull_subset)
   11.14  
   11.15  
   11.16 -subsection%unimportant \<open>Openness and compactness are preserved by convex hull operation.\<close>
   11.17 +subsection%unimportant \<open>Openness and compactness are preserved by convex hull operation\<close>
   11.18  
   11.19  lemma open_convex_hull[intro]:
   11.20    fixes s :: "'a::real_normed_vector set"
   11.21 @@ -5422,7 +5422,7 @@
   11.22  qed
   11.23  
   11.24  
   11.25 -subsection%unimportant \<open>Extremal points of a simplex are some vertices.\<close>
   11.26 +subsection%unimportant \<open>Extremal points of a simplex are some vertices\<close>
   11.27  
   11.28  lemma dist_increases_online:
   11.29    fixes a b d :: "'a::real_inner"
   11.30 @@ -5621,7 +5621,7 @@
   11.31    by(cases "s = {}") auto
   11.32  
   11.33  
   11.34 -subsection \<open>Closest point of a convex set is unique, with a continuous projection.\<close>
   11.35 +subsection \<open>Closest point of a convex set is unique, with a continuous projection\<close>
   11.36  
   11.37  definition%important closest_point :: "'a::{real_inner,heine_borel} set \<Rightarrow> 'a \<Rightarrow> 'a"
   11.38    where "closest_point s a = (SOME x. x \<in> s \<and> (\<forall>y\<in>s. dist a x \<le> dist a y))"
   11.39 @@ -5811,7 +5811,7 @@
   11.40  qed
   11.41  
   11.42  
   11.43 -subsubsection%unimportant \<open>Various point-to-set separating/supporting hyperplane theorems.\<close>
   11.44 +subsubsection%unimportant \<open>Various point-to-set separating/supporting hyperplane theorems\<close>
   11.45  
   11.46  lemma supporting_hyperplane_closed_point:
   11.47    fixes z :: "'a::{real_inner,heine_borel}"
   11.48 @@ -6132,7 +6132,7 @@
   11.49    using hull_subset[of s convex] convex_hull_empty by auto
   11.50  
   11.51  
   11.52 -subsection%unimportant \<open>Moving and scaling convex hulls.\<close>
   11.53 +subsection%unimportant \<open>Moving and scaling convex hulls\<close>
   11.54  
   11.55  lemma convex_hull_set_plus:
   11.56    "convex hull (s + t) = convex hull s + convex hull t"
   11.57 @@ -6657,7 +6657,7 @@
   11.58       "\<lbrakk>connected S; aff_dim S \<noteq> 0; a \<in> S\<rbrakk> \<Longrightarrow> a islimpt S"
   11.59    using aff_dim_sing connected_imp_perfect by blast
   11.60  
   11.61 -subsection%unimportant \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close>
   11.62 +subsection%unimportant \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent\<close>
   11.63  
   11.64  lemma mem_is_interval_1_I:
   11.65    fixes a b c::real
    12.1 --- a/src/HOL/Analysis/Derivative.thy	Sun Apr 08 12:31:08 2018 +0200
    12.2 +++ b/src/HOL/Analysis/Derivative.thy	Mon Apr 09 16:20:23 2018 +0200
    12.3 @@ -15,7 +15,7 @@
    12.4  
    12.5  subsection \<open>Derivatives\<close>
    12.6  
    12.7 -subsubsection \<open>Combining theorems.\<close>
    12.8 +subsubsection \<open>Combining theorems\<close>
    12.9  
   12.10  lemmas has_derivative_id = has_derivative_ident
   12.11  lemmas has_derivative_neg = has_derivative_minus
   12.12 @@ -32,7 +32,7 @@
   12.13    by (intro derivative_eq_intros) auto
   12.14  
   12.15  
   12.16 -subsection \<open>Derivative with composed bilinear function.\<close>
   12.17 +subsection \<open>Derivative with composed bilinear function\<close>
   12.18  
   12.19  lemma has_derivative_bilinear_within:
   12.20    assumes "(f has_derivative f') (at x within s)"
    13.1 --- a/src/HOL/Analysis/Determinants.thy	Sun Apr 08 12:31:08 2018 +0200
    13.2 +++ b/src/HOL/Analysis/Determinants.thy	Mon Apr 09 16:20:23 2018 +0200
    13.3 @@ -929,7 +929,7 @@
    13.4      by auto
    13.5  qed
    13.6  
    13.7 -subsection \<open>Orthogonality of a transformation and matrix.\<close>
    13.8 +subsection \<open>Orthogonality of a transformation and matrix\<close>
    13.9  
   13.10  definition "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
   13.11  
   13.12 @@ -1087,7 +1087,7 @@
   13.13    using det_orthogonal_matrix orthogonal_transformation_matrix by fastforce
   13.14  
   13.15  
   13.16 -subsection \<open>Linearity of scaling, and hence isometry, that preserves origin.\<close>
   13.17 +subsection \<open>Linearity of scaling, and hence isometry, that preserves origin\<close>
   13.18  
   13.19  lemma scaling_linear:
   13.20    fixes f :: "'a::real_inner \<Rightarrow> 'a::real_inner"
   13.21 @@ -1157,7 +1157,7 @@
   13.22      by (auto simp: orthogonal_transformation_isometry)
   13.23  qed
   13.24  
   13.25 -subsection\<open> We can find an orthogonal matrix taking any unit vector to any other.\<close>
   13.26 +subsection\<open> We can find an orthogonal matrix taking any unit vector to any other\<close>
   13.27  
   13.28  lemma orthogonal_matrix_transpose [simp]:
   13.29       "orthogonal_matrix(transpose A) \<longleftrightarrow> orthogonal_matrix A"
   13.30 @@ -1251,7 +1251,7 @@
   13.31  qed
   13.32  
   13.33  
   13.34 -subsection \<open>Can extend an isometry from unit sphere.\<close>
   13.35 +subsection \<open>Can extend an isometry from unit sphere\<close>
   13.36  
   13.37  lemma isometry_sphere_extend:
   13.38    fixes f:: "'a::real_inner \<Rightarrow> 'a"
   13.39 @@ -1349,7 +1349,7 @@
   13.40      done
   13.41  qed
   13.42  
   13.43 -subsection \<open>Rotation, reflection, rotoinversion.\<close>
   13.44 +subsection \<open>Rotation, reflection, rotoinversion\<close>
   13.45  
   13.46  definition "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
   13.47  definition "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
    14.1 --- a/src/HOL/Analysis/Fashoda_Theorem.thy	Sun Apr 08 12:31:08 2018 +0200
    14.2 +++ b/src/HOL/Analysis/Fashoda_Theorem.thy	Mon Apr 09 16:20:23 2018 +0200
    14.3 @@ -8,7 +8,7 @@
    14.4  imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
    14.5  begin
    14.6  
    14.7 -subsection \<open>Bijections between intervals.\<close>
    14.8 +subsection \<open>Bijections between intervals\<close>
    14.9  
   14.10  definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
   14.11    where "interval_bij =
    15.1 --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Sun Apr 08 12:31:08 2018 +0200
    15.2 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Mon Apr 09 16:20:23 2018 +0200
    15.3 @@ -2,7 +2,7 @@
    15.4      Author:     Amine Chaieb, University of Cambridge
    15.5  *)
    15.6  
    15.7 -section \<open>Definition of finite Cartesian product types.\<close>
    15.8 +section \<open>Definition of finite Cartesian product types\<close>
    15.9  
   15.10  theory Finite_Cartesian_Product
   15.11  imports
   15.12 @@ -13,7 +13,7 @@
   15.13    "HOL-Library.FuncSet"
   15.14  begin
   15.15  
   15.16 -subsection \<open>Finite Cartesian products, with indexing and lambdas.\<close>
   15.17 +subsection \<open>Finite Cartesian products, with indexing and lambdas\<close>
   15.18  
   15.19  typedef ('a, 'b) vec = "UNIV :: ('b::finite \<Rightarrow> 'a) set"
   15.20    morphisms vec_nth vec_lambda ..
    16.1 --- a/src/HOL/Analysis/Further_Topology.thy	Sun Apr 08 12:31:08 2018 +0200
    16.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Mon Apr 09 16:20:23 2018 +0200
    16.3 @@ -1,4 +1,4 @@
    16.4 -section \<open>Extending Continous Maps, Invariance of Domain, etc..\<close>
    16.5 +section \<open>Extending Continous Maps, Invariance of Domain, etc\<close>
    16.6  
    16.7  text\<open>Ported from HOL Light (moretop.ml) by L C Paulson\<close>
    16.8  
    16.9 @@ -367,7 +367,7 @@
   16.10  
   16.11  
   16.12  
   16.13 -subsection\<open> Some technical lemmas about extending maps from cell complexes.\<close>
   16.14 +subsection\<open> Some technical lemmas about extending maps from cell complexes\<close>
   16.15  
   16.16  lemma extending_maps_Union_aux:
   16.17    assumes fin: "finite \<F>"
   16.18 @@ -981,7 +981,7 @@
   16.19  
   16.20  
   16.21  
   16.22 -subsection\<open> Special cases and corollaries involving spheres.\<close>
   16.23 +subsection\<open> Special cases and corollaries involving spheres\<close>
   16.24  
   16.25  lemma disjnt_Diff1: "X \<subseteq> Y' \<Longrightarrow> disjnt (X - Y) (X' - Y')"
   16.26    by (auto simp: disjnt_def)
   16.27 @@ -2727,7 +2727,7 @@
   16.28      using clopen [of S] False  by simp
   16.29  qed
   16.30  
   16.31 -subsection\<open> Dimension-based conditions for various homeomorphisms.\<close>
   16.32 +subsection\<open>Dimension-based conditions for various homeomorphisms\<close>
   16.33  
   16.34  lemma homeomorphic_subspaces_eq:
   16.35    fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
   16.36 @@ -3896,7 +3896,7 @@
   16.37  qed
   16.38  
   16.39  
   16.40 -subsection\<open>Another simple case where sphere maps are nullhomotopic.\<close>
   16.41 +subsection\<open>Another simple case where sphere maps are nullhomotopic\<close>
   16.42  
   16.43  lemma inessential_spheremap_2_aux:
   16.44    fixes f :: "'a::euclidean_space \<Rightarrow> complex"
   16.45 @@ -3962,7 +3962,7 @@
   16.46  qed
   16.47  
   16.48  
   16.49 -subsection\<open>Holomorphic logarithms and square roots.\<close>
   16.50 +subsection\<open>Holomorphic logarithms and square roots\<close>
   16.51  
   16.52  lemma contractible_imp_holomorphic_log:
   16.53    assumes holf: "f holomorphic_on S"
    17.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Apr 08 12:31:08 2018 +0200
    17.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Apr 09 16:20:23 2018 +0200
    17.3 @@ -3,7 +3,7 @@
    17.4                  Huge cleanup by LCP
    17.5  *)
    17.6  
    17.7 -section \<open>Henstock-Kurzweil gauge integration in many dimensions.\<close>
    17.8 +section \<open>Henstock-Kurzweil gauge integration in many dimensions\<close>
    17.9  
   17.10  theory Henstock_Kurzweil_Integration
   17.11  imports
   17.12 @@ -28,7 +28,7 @@
   17.13    by blast
   17.14  (* END MOVE *)
   17.15  
   17.16 -subsection \<open>Content (length, area, volume...) of an interval.\<close>
   17.17 +subsection \<open>Content (length, area, volume...) of an interval\<close>
   17.18  
   17.19  abbreviation content :: "'a::euclidean_space set \<Rightarrow> real"
   17.20    where "content s \<equiv> measure lborel s"
   17.21 @@ -313,7 +313,7 @@
   17.22  lemma has_integral_integral: "f integrable_on s \<longleftrightarrow> (f has_integral (integral s f)) s"
   17.23    by auto
   17.24  
   17.25 -subsection \<open>Basic theorems about integrals.\<close>
   17.26 +subsection \<open>Basic theorems about integrals\<close>
   17.27  
   17.28  lemma has_integral_eq_rhs: "(f has_integral j) S \<Longrightarrow> i = j \<Longrightarrow> (f has_integral i) S"
   17.29    by (rule forw_subst)
   17.30 @@ -909,7 +909,7 @@
   17.31  
   17.32  
   17.33  
   17.34 -subsection \<open>Cauchy-type criterion for integrability.\<close>
   17.35 +subsection \<open>Cauchy-type criterion for integrability\<close>
   17.36  
   17.37  proposition integrable_Cauchy:
   17.38    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::{real_normed_vector,complete_space}"
   17.39 @@ -1012,7 +1012,7 @@
   17.40  qed
   17.41  
   17.42  
   17.43 -subsection \<open>Additivity of integral on abutting intervals.\<close>
   17.44 +subsection \<open>Additivity of integral on abutting intervals\<close>
   17.45  
   17.46  lemma tagged_division_split_left_inj_content:
   17.47    assumes \<D>: "\<D> tagged_division_of S"
   17.48 @@ -1261,7 +1261,7 @@
   17.49  qed
   17.50  
   17.51  
   17.52 -subsection \<open>A sort of converse, integrability on subintervals.\<close>
   17.53 +subsection \<open>A sort of converse, integrability on subintervals\<close>
   17.54  
   17.55  lemma has_integral_separate_sides:
   17.56    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   17.57 @@ -1459,7 +1459,7 @@
   17.58    qed
   17.59  qed
   17.60  
   17.61 -subsection \<open>Bounds on the norm of Riemann sums and the integral itself.\<close>
   17.62 +subsection \<open>Bounds on the norm of Riemann sums and the integral itself\<close>
   17.63  
   17.64  lemma dsum_bound:
   17.65    assumes "p division_of (cbox a b)"
   17.66 @@ -1562,7 +1562,7 @@
   17.67  by (metis integrable_integral has_integral_bound assms)
   17.68  
   17.69  
   17.70 -subsection \<open>Similar theorems about relationship among components.\<close>
   17.71 +subsection \<open>Similar theorems about relationship among components\<close>
   17.72  
   17.73  lemma rsum_component_le:
   17.74    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   17.75 @@ -1764,7 +1764,7 @@
   17.76    using assms
   17.77    by (metis box_real(2) integral_component_ubound)
   17.78  
   17.79 -subsection \<open>Uniform limit of integrable functions is integrable.\<close>
   17.80 +subsection \<open>Uniform limit of integrable functions is integrable\<close>
   17.81  
   17.82  lemma real_arch_invD:
   17.83    "0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
   17.84 @@ -1907,13 +1907,13 @@
   17.85  lemmas integrable_uniform_limit_real = integrable_uniform_limit [where 'a=real, simplified]
   17.86  
   17.87  
   17.88 -subsection \<open>Negligible sets.\<close>
   17.89 +subsection \<open>Negligible sets\<close>
   17.90  
   17.91  definition "negligible (s:: 'a::euclidean_space set) \<longleftrightarrow>
   17.92    (\<forall>a b. ((indicator s :: 'a\<Rightarrow>real) has_integral 0) (cbox a b))"
   17.93  
   17.94  
   17.95 -subsubsection \<open>Negligibility of hyperplane.\<close>
   17.96 +subsubsection \<open>Negligibility of hyperplane\<close>
   17.97  
   17.98  lemma content_doublesplit:
   17.99    fixes a :: "'a::euclidean_space"
  17.100 @@ -2082,7 +2082,7 @@
  17.101  qed
  17.102  
  17.103  
  17.104 -subsubsection \<open>Hence the main theorem about negligible sets.\<close>
  17.105 +subsubsection \<open>Hence the main theorem about negligible sets\<close>
  17.106  
  17.107  
  17.108  lemma has_integral_negligible_cbox:
  17.109 @@ -2276,7 +2276,7 @@
  17.110      by (auto simp: integral_def integrable_on_def)
  17.111  
  17.112  
  17.113 -subsection \<open>Some other trivialities about negligible sets.\<close>
  17.114 +subsection \<open>Some other trivialities about negligible sets\<close>
  17.115  
  17.116  lemma negligible_subset:
  17.117    assumes "negligible s" "t \<subseteq> s"
  17.118 @@ -2366,7 +2366,7 @@
  17.119  qed auto
  17.120  
  17.121  
  17.122 -subsection \<open>Finite case of the spike theorem is quite commonly needed.\<close>
  17.123 +subsection \<open>Finite case of the spike theorem is quite commonly needed\<close>
  17.124  
  17.125  lemma has_integral_spike_finite:
  17.126    assumes "finite S"
  17.127 @@ -2414,7 +2414,7 @@
  17.128    by (metis assms box_real(2) has_integral_bound_spike_finite)
  17.129  
  17.130  
  17.131 -subsection \<open>In particular, the boundary of an interval is negligible.\<close>
  17.132 +subsection \<open>In particular, the boundary of an interval is negligible\<close>
  17.133  
  17.134  lemma negligible_frontier_interval: "negligible(cbox (a::'a::euclidean_space) b - box a b)"
  17.135  proof -
  17.136 @@ -2445,7 +2445,7 @@
  17.137    using assms has_integral_spike_interior_eq by blast
  17.138  
  17.139  
  17.140 -subsection \<open>Integrability of continuous functions.\<close>
  17.141 +subsection \<open>Integrability of continuous functions\<close>
  17.142  
  17.143  lemma operative_approximableI:
  17.144    fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
  17.145 @@ -2573,10 +2573,10 @@
  17.146    by (auto intro!: integrable_continuous_interval simp: closed_segment_eq_real_ivl)
  17.147  
  17.148  
  17.149 -subsection \<open>Specialization of additivity to one dimension.\<close>
  17.150 -
  17.151 -
  17.152 -subsection \<open>A useful lemma allowing us to factor out the content size.\<close>
  17.153 +subsection \<open>Specialization of additivity to one dimension\<close>
  17.154 +
  17.155 +
  17.156 +subsection \<open>A useful lemma allowing us to factor out the content size\<close>
  17.157  
  17.158  lemma has_integral_factor_content:
  17.159    "(f has_integral i) (cbox a b) \<longleftrightarrow>
  17.160 @@ -2642,7 +2642,7 @@
  17.161    by (rule has_integral_factor_content)
  17.162  
  17.163  
  17.164 -subsection \<open>Fundamental theorem of calculus.\<close>
  17.165 +subsection \<open>Fundamental theorem of calculus\<close>
  17.166  
  17.167  lemma interval_bounds_real:
  17.168    fixes q b :: real
  17.169 @@ -2884,7 +2884,7 @@
  17.170  qed
  17.171  
  17.172  
  17.173 -subsection \<open>Only need trivial subintervals if the interval itself is trivial.\<close>
  17.174 +subsection \<open>Only need trivial subintervals if the interval itself is trivial\<close>
  17.175  
  17.176  proposition division_of_nontrivial:
  17.177    fixes \<D> :: "'a::euclidean_space set set"
  17.178 @@ -2970,7 +2970,7 @@
  17.179  qed
  17.180  
  17.181  
  17.182 -subsection \<open>Integrability on subintervals.\<close>
  17.183 +subsection \<open>Integrability on subintervals\<close>
  17.184  
  17.185  lemma operative_integrableI:
  17.186    fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
  17.187 @@ -3016,7 +3016,7 @@
  17.188    shows "f integrable_on {c..d}"
  17.189    by (metis assms box_real(2) integrable_subinterval)
  17.190  
  17.191 -subsection \<open>Combining adjacent intervals in 1 dimension.\<close>
  17.192 +subsection \<open>Combining adjacent intervals in 1 dimension\<close>
  17.193  
  17.194  lemma has_integral_combine:
  17.195    fixes a b c :: real and j :: "'a::banach"
  17.196 @@ -3087,7 +3087,7 @@
  17.197    using integral_combine[of b a c f] integral_combine[of a b c f]
  17.198    by (auto simp: algebra_simps min_def)
  17.199  
  17.200 -subsection \<open>Reduce integrability to "local" integrability.\<close>
  17.201 +subsection \<open>Reduce integrability to "local" integrability\<close>
  17.202  
  17.203  lemma integrable_on_little_subintervals:
  17.204    fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
  17.205 @@ -3116,7 +3116,7 @@
  17.206  qed
  17.207  
  17.208  
  17.209 -subsection \<open>Second FTC or existence of antiderivative.\<close>
  17.210 +subsection \<open>Second FTC or existence of antiderivative\<close>
  17.211  
  17.212  lemma integrable_const[intro]: "(\<lambda>x. c) integrable_on cbox a b"
  17.213    unfolding integrable_on_def by blast
  17.214 @@ -3204,7 +3204,7 @@
  17.215    obtains g where "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative (f x::_::banach)) (at x within {a..b})"
  17.216    using integral_has_vector_derivative[OF assms] by auto
  17.217  
  17.218 -subsection \<open>Combined fundamental theorem of calculus.\<close>
  17.219 +subsection \<open>Combined fundamental theorem of calculus\<close>
  17.220  
  17.221  lemma antiderivative_integral_continuous:
  17.222    fixes f :: "real \<Rightarrow> 'a::banach"
  17.223 @@ -3227,7 +3227,7 @@
  17.224  qed
  17.225  
  17.226  
  17.227 -subsection \<open>General "twiddling" for interval-to-interval function image.\<close>
  17.228 +subsection \<open>General "twiddling" for interval-to-interval function image\<close>
  17.229  
  17.230  lemma has_integral_twiddle:
  17.231    assumes "0 < r"
  17.232 @@ -3334,7 +3334,7 @@
  17.233  qed
  17.234  
  17.235  
  17.236 -subsection \<open>Special case of a basic affine transformation.\<close>
  17.237 +subsection \<open>Special case of a basic affine transformation\<close>
  17.238  
  17.239  lemma AE_lborel_inner_neq:
  17.240    assumes k: "k \<in> Basis"
  17.241 @@ -3460,7 +3460,7 @@
  17.242  
  17.243  lemmas has_integral_affinity01 = has_integral_affinity [of _ _ 0 "1::real", simplified]
  17.244  
  17.245 -subsection \<open>Special case of stretching coordinate axes separately.\<close>
  17.246 +subsection \<open>Special case of stretching coordinate axes separately\<close>
  17.247  
  17.248  lemma has_integral_stretch:
  17.249    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
  17.250 @@ -3485,7 +3485,7 @@
  17.251    by (force dest: has_integral_stretch)
  17.252  
  17.253  
  17.254 -subsection \<open>even more special cases.\<close>
  17.255 +subsection \<open>even more special cases\<close>
  17.256  
  17.257  lemma uminus_interval_vector[simp]:
  17.258    fixes a b :: "'a::euclidean_space"
  17.259 @@ -3528,7 +3528,7 @@
  17.260    by (rule integral_reflect)
  17.261  
  17.262  
  17.263 -subsection \<open>Stronger form of FCT; quite a tedious proof.\<close>
  17.264 +subsection \<open>Stronger form of FCT; quite a tedious proof\<close>
  17.265  
  17.266  lemma split_minus[simp]: "(\<lambda>(x, k). f x k) x - (\<lambda>(x, k). g x k) x = (\<lambda>(x, k). f x k - g x k) x"
  17.267    by (simp add: split_def)
  17.268 @@ -3904,7 +3904,7 @@
  17.269  qed
  17.270  
  17.271  
  17.272 -subsection \<open>Stronger form with finite number of exceptional points.\<close>
  17.273 +subsection \<open>Stronger form with finite number of exceptional points\<close>
  17.274  
  17.275  lemma fundamental_theorem_of_calculus_interior_strong:
  17.276    fixes f :: "real \<Rightarrow> 'a::banach"
  17.277 @@ -4217,7 +4217,7 @@
  17.278    by (auto simp: has_field_derivative_iff_has_vector_derivative)
  17.279  
  17.280  
  17.281 -subsection \<open>This doesn't directly involve integration, but that gives an easy proof.\<close>
  17.282 +subsection \<open>This doesn't directly involve integration, but that gives an easy proof\<close>
  17.283  
  17.284  lemma has_derivative_zero_unique_strong_interval:
  17.285    fixes f :: "real \<Rightarrow> 'a::banach"
  17.286 @@ -4251,7 +4251,7 @@
  17.287  qed
  17.288  
  17.289  
  17.290 -subsection \<open>Generalize a bit to any convex set.\<close>
  17.291 +subsection \<open>Generalize a bit to any convex set\<close>
  17.292  
  17.293  lemma has_derivative_zero_unique_strong_convex:
  17.294    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
  17.295 @@ -4919,7 +4919,7 @@
  17.296  qed
  17.297  
  17.298  
  17.299 -subsection \<open>Continuity of the integral (for a 1-dimensional interval).\<close>
  17.300 +subsection \<open>Continuity of the integral (for a 1-dimensional interval)\<close>
  17.301  
  17.302  lemma integrable_alt:
  17.303    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
    18.1 --- a/src/HOL/Analysis/Jordan_Curve.thy	Sun Apr 08 12:31:08 2018 +0200
    18.2 +++ b/src/HOL/Analysis/Jordan_Curve.thy	Mon Apr 09 16:20:23 2018 +0200
    18.3 @@ -9,7 +9,7 @@
    18.4  
    18.5  begin
    18.6  
    18.7 -subsection\<open>Janiszewski's theorem.\<close>
    18.8 +subsection\<open>Janiszewski's theorem\<close>
    18.9  
   18.10  lemma Janiszewski_weak:
   18.11    fixes a b::complex
    19.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Sun Apr 08 12:31:08 2018 +0200
    19.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Apr 09 16:20:23 2018 +0200
    19.3 @@ -978,7 +978,8 @@
    19.4    then show ?thesis
    19.5      by (auto dest!: AE_not_in)
    19.6  qed
    19.7 -subsection\<open> A nice lemma for negligibility proofs.\<close>
    19.8 +
    19.9 +subsection \<open>A nice lemma for negligibility proofs\<close>
   19.10  
   19.11  lemma summable_iff_suminf_neq_top: "(\<And>n. f n \<ge> 0) \<Longrightarrow> \<not> summable f \<Longrightarrow> (\<Sum>i. ennreal (f i)) = top"
   19.12    by (metis summable_suminf_not_top)
    20.1 --- a/src/HOL/Analysis/Path_Connected.thy	Sun Apr 08 12:31:08 2018 +0200
    20.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Mon Apr 09 16:20:23 2018 +0200
    20.3 @@ -3380,7 +3380,7 @@
    20.4        by (metis dw_le norm_minus_commute not_less order_trans rle wy)
    20.5  qed
    20.6  
    20.7 -section\<open> Homotopy of maps p,q : X=>Y with property P of all intermediate maps.\<close>
    20.8 +section\<open> Homotopy of maps p,q : X=>Y with property P of all intermediate maps\<close>
    20.9  
   20.10  text%important\<open> We often just want to require that it fixes some subset, but to take in
   20.11    the case of a loop homotopy, it's convenient to have a general property P.\<close>
   20.12 @@ -3487,7 +3487,7 @@
   20.13  qed
   20.14  
   20.15  
   20.16 -subsection%unimportant\<open> Trivial properties.\<close>
   20.17 +subsection%unimportant\<open>Trivial properties\<close>
   20.18  
   20.19  lemma homotopic_with_imp_property: "homotopic_with P X Y f g \<Longrightarrow> P f \<and> P g"
   20.20    unfolding homotopic_with_def Ball_def
   20.21 @@ -3742,7 +3742,7 @@
   20.22  qed
   20.23  
   20.24  
   20.25 -subsection\<open>Homotopy of paths, maintaining the same endpoints.\<close>
   20.26 +subsection\<open>Homotopy of paths, maintaining the same endpoints\<close>
   20.27  
   20.28  
   20.29  definition%important homotopic_paths :: "['a set, real \<Rightarrow> 'a, real \<Rightarrow> 'a::topological_space] \<Rightarrow> bool"
   20.30 @@ -3958,7 +3958,7 @@
   20.31  using%unimportant homotopic_paths_rinv [of "reversepath p" s] assms by simp
   20.32  
   20.33  
   20.34 -subsection\<open> Homotopy of loops without requiring preservation of endpoints.\<close>
   20.35 +subsection\<open>Homotopy of loops without requiring preservation of endpoints\<close>
   20.36  
   20.37  definition%important homotopic_loops :: "'a::topological_space set \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool"  where
   20.38   "homotopic_loops s p q \<equiv>
   20.39 @@ -4197,7 +4197,7 @@
   20.40  qed
   20.41  
   20.42  
   20.43 -subsection%unimportant\<open> Homotopy of "nearby" function, paths and loops.\<close>
   20.44 +subsection%unimportant\<open>Homotopy of "nearby" function, paths and loops\<close>
   20.45  
   20.46  lemma homotopic_with_linear:
   20.47    fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
   20.48 @@ -5521,7 +5521,7 @@
   20.49      by (metis open_openin openin_topspace subtopology_superset top.extremum topspace_euclidean_subtopology)
   20.50  qed
   20.51  
   20.52 -subsection\<open>Sura-Bura's results about compact components of sets.\<close>
   20.53 +subsection\<open>Sura-Bura's results about compact components of sets\<close>
   20.54  
   20.55  proposition Sura_Bura_compact:
   20.56    fixes S :: "'a::euclidean_space set"
   20.57 @@ -7452,7 +7452,7 @@
   20.58  
   20.59  
   20.60  
   20.61 -subsection\<open> Self-homeomorphisms shuffling points about in various ways.\<close>
   20.62 +subsection\<open>Self-homeomorphisms shuffling points about in various ways\<close>
   20.63  
   20.64  subsubsection%unimportant\<open>The theorem \<open>homeomorphism_moving_points_exists\<close>\<close>
   20.65  
    21.1 --- a/src/HOL/Analysis/Poly_Roots.thy	Sun Apr 08 12:31:08 2018 +0200
    21.2 +++ b/src/HOL/Analysis/Poly_Roots.thy	Mon Apr 09 16:20:23 2018 +0200
    21.3 @@ -8,7 +8,7 @@
    21.4  imports Complex_Main
    21.5  begin
    21.6  
    21.7 -subsection\<open>Basics about polynomial functions: extremal behaviour and root counts.\<close>
    21.8 +subsection\<open>Basics about polynomial functions: extremal behaviour and root counts\<close>
    21.9  
   21.10  lemma sub_polyfun:
   21.11    fixes x :: "'a::{comm_ring,monoid_mult}"
    22.1 --- a/src/HOL/Analysis/Polytope.thy	Sun Apr 08 12:31:08 2018 +0200
    22.2 +++ b/src/HOL/Analysis/Polytope.thy	Mon Apr 09 16:20:23 2018 +0200
    22.3 @@ -1,4 +1,4 @@
    22.4 -section \<open>Faces, Extreme Points, Polytopes, Polyhedra etc.\<close>
    22.5 +section \<open>Faces, Extreme Points, Polytopes, Polyhedra etc\<close>
    22.6  
    22.7  text\<open>Ported from HOL Light by L C Paulson\<close>
    22.8  
    23.1 --- a/src/HOL/Analysis/Riemann_Mapping.thy	Sun Apr 08 12:31:08 2018 +0200
    23.2 +++ b/src/HOL/Analysis/Riemann_Mapping.thy	Mon Apr 09 16:20:23 2018 +0200
    23.3 @@ -8,7 +8,7 @@
    23.4  imports Great_Picard
    23.5  begin
    23.6  
    23.7 -subsection\<open>Moebius functions are biholomorphisms of the unit disc.\<close>
    23.8 +subsection\<open>Moebius functions are biholomorphisms of the unit disc\<close>
    23.9  
   23.10  definition Moebius_function :: "[real,complex,complex] \<Rightarrow> complex" where
   23.11    "Moebius_function \<equiv> \<lambda>t w z. exp(\<i> * of_real t) * (z - w) / (1 - cnj w * z)"
   23.12 @@ -853,7 +853,7 @@
   23.13    using convex_imp_contractible homeomorphic_contractible_eq simply_connected_eq_homeomorphic_to_disc by auto
   23.14  
   23.15  
   23.16 -subsection\<open>A further chain of equivalences about components of the complement of a simply connected set.\<close>
   23.17 +subsection\<open>A further chain of equivalences about components of the complement of a simply connected set\<close>
   23.18  
   23.19  text\<open>(following 1.35 in Burckel'S book)\<close>
   23.20  
    24.1 --- a/src/HOL/Analysis/Starlike.thy	Sun Apr 08 12:31:08 2018 +0200
    24.2 +++ b/src/HOL/Analysis/Starlike.thy	Mon Apr 09 16:20:23 2018 +0200
    24.3 @@ -6,7 +6,7 @@
    24.4     Author:     Johannes Hoelzl, TU Muenchen
    24.5  *)
    24.6  
    24.7 -section \<open>Line segments, Starlike Sets, etc.\<close>
    24.8 +section \<open>Line segments, Starlike Sets, etc\<close>
    24.9  
   24.10  theory Starlike
   24.11    imports Convex_Euclidean_Space
   24.12 @@ -4157,7 +4157,7 @@
   24.13      by (metis Diff_cancel convex_hull_singleton insert_absorb2 open_segment_def segment_convex_hull)
   24.14  qed
   24.15  
   24.16 -subsection%unimportant\<open>Similar results for closure and (relative or absolute) frontier.\<close>
   24.17 +subsection%unimportant\<open>Similar results for closure and (relative or absolute) frontier\<close>
   24.18  
   24.19  lemma closure_convex_hull [simp]:
   24.20    fixes s :: "'a::euclidean_space set"
   24.21 @@ -7119,7 +7119,7 @@
   24.22    done
   24.23  qed
   24.24  
   24.25 -subsection\<open>Decomposing a vector into parts in orthogonal subspaces.\<close>
   24.26 +subsection\<open>Decomposing a vector into parts in orthogonal subspaces\<close>
   24.27  
   24.28  text\<open>existence of orthonormal basis for a subspace.\<close>
   24.29  
   24.30 @@ -7470,7 +7470,7 @@
   24.31    finally show "dim T \<le> dim S" by simp
   24.32  qed
   24.33  
   24.34 -subsection\<open>Lower-dimensional affine subsets are nowhere dense.\<close>
   24.35 +subsection\<open>Lower-dimensional affine subsets are nowhere dense\<close>
   24.36  
   24.37  proposition%important dense_complement_subspace:
   24.38    fixes S :: "'a :: euclidean_space set"
   24.39 @@ -7583,7 +7583,7 @@
   24.40    by (simp add: assms dense_complement_convex)
   24.41  
   24.42  
   24.43 -subsection%unimportant\<open>Parallel slices, etc.\<close>
   24.44 +subsection%unimportant\<open>Parallel slices, etc\<close>
   24.45  
   24.46  text\<open> If we take a slice out of a set, we can do it perpendicularly,
   24.47    with the normal vector to the slice parallel to the affine hull.\<close>
    25.1 --- a/src/HOL/Analysis/Tagged_Division.thy	Sun Apr 08 12:31:08 2018 +0200
    25.2 +++ b/src/HOL/Analysis/Tagged_Division.thy	Mon Apr 09 16:20:23 2018 +0200
    25.3 @@ -55,7 +55,7 @@
    25.4      by (simp add: field_simps)
    25.5  qed
    25.6  
    25.7 -subsection \<open>Some useful lemmas about intervals.\<close>
    25.8 +subsection \<open>Some useful lemmas about intervals\<close>
    25.9  
   25.10  lemma interior_subset_union_intervals:
   25.11    assumes "i = cbox a b"
   25.12 @@ -130,7 +130,7 @@
   25.13  lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
   25.14    by (simp add: box_ne_empty)
   25.15  
   25.16 -subsection \<open>Bounds on intervals where they exist.\<close>
   25.17 +subsection \<open>Bounds on intervals where they exist\<close>
   25.18  
   25.19  definition interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
   25.20    where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
   25.21 @@ -192,7 +192,7 @@
   25.22        by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
   25.23  qed
   25.24  
   25.25 -subsection \<open>The notion of a gauge --- simply an open set containing the point.\<close>
   25.26 +subsection \<open>The notion of a gauge --- simply an open set containing the point\<close>
   25.27  
   25.28  definition "gauge \<gamma> \<longleftrightarrow> (\<forall>x. x \<in> \<gamma> x \<and> open (\<gamma> x))"
   25.29  
   25.30 @@ -242,14 +242,14 @@
   25.31    "(\<forall>x. \<exists>d :: real. p x \<longrightarrow> 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. p x \<longrightarrow> q d x)"
   25.32    by (metis zero_less_one)
   25.33  
   25.34 -subsection \<open>Attempt a systematic general set of "offset" results for components.\<close>
   25.35 +subsection \<open>Attempt a systematic general set of "offset" results for components\<close>
   25.36  
   25.37  lemma gauge_modify:
   25.38    assumes "(\<forall>S. open S \<longrightarrow> open {x. f(x) \<in> S})" "gauge d"
   25.39    shows "gauge (\<lambda>x. {y. f y \<in> d (f x)})"
   25.40    using assms unfolding gauge_def by force
   25.41  
   25.42 -subsection \<open>Divisions.\<close>
   25.43 +subsection \<open>Divisions\<close>
   25.44  
   25.45  definition division_of (infixl "division'_of" 40)
   25.46  where
   25.47 @@ -995,7 +995,7 @@
   25.48    }
   25.49  qed
   25.50  
   25.51 -subsection \<open>Tagged (partial) divisions.\<close>
   25.52 +subsection \<open>Tagged (partial) divisions\<close>
   25.53  
   25.54  definition tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40)
   25.55    where "s tagged_partial_division_of i \<longleftrightarrow>
   25.56 @@ -1828,7 +1828,7 @@
   25.57  qed
   25.58  
   25.59  
   25.60 -subsection \<open>Special case of additivity we need for the FTC.\<close>
   25.61 +subsection \<open>Special case of additivity we need for the FTC\<close>
   25.62  
   25.63  lemma additive_tagged_division_1:
   25.64    fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
   25.65 @@ -1856,7 +1856,7 @@
   25.66  qed
   25.67  
   25.68  
   25.69 -subsection \<open>Fine-ness of a partition w.r.t. a gauge.\<close>
   25.70 +subsection \<open>Fine-ness of a partition w.r.t. a gauge\<close>
   25.71  
   25.72  definition fine  (infixr "fine" 46)
   25.73    where "d fine s \<longleftrightarrow> (\<forall>(x,k) \<in> s. k \<subseteq> d x)"
   25.74 @@ -1887,7 +1887,7 @@
   25.75  lemma fine_subset: "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p"
   25.76    unfolding fine_def by blast
   25.77  
   25.78 -subsection \<open>Some basic combining lemmas.\<close>
   25.79 +subsection \<open>Some basic combining lemmas\<close>
   25.80  
   25.81  lemma tagged_division_Union_exists:
   25.82    assumes "finite I"
   25.83 @@ -1907,14 +1907,14 @@
   25.84  qed
   25.85  
   25.86  
   25.87 -subsection \<open>The set we're concerned with must be closed.\<close>
   25.88 +subsection \<open>The set we're concerned with must be closed\<close>
   25.89  
   25.90  lemma division_of_closed:
   25.91    fixes i :: "'n::euclidean_space set"
   25.92    shows "s division_of i \<Longrightarrow> closed i"
   25.93    unfolding division_of_def by fastforce
   25.94  
   25.95 -subsection \<open>General bisection principle for intervals; might be useful elsewhere.\<close>
   25.96 +subsection \<open>General bisection principle for intervals; might be useful elsewhere\<close>
   25.97  
   25.98  lemma interval_bisection_step:
   25.99    fixes type :: "'a::euclidean_space"
  25.100 @@ -2185,7 +2185,7 @@
  25.101  qed
  25.102  
  25.103  
  25.104 -subsection \<open>Cousin's lemma.\<close>
  25.105 +subsection \<open>Cousin's lemma\<close>
  25.106  
  25.107  lemma fine_division_exists:
  25.108    fixes a b :: "'a::euclidean_space"
  25.109 @@ -2231,7 +2231,7 @@
  25.110    obtains p where "p tagged_division_of {a .. b}" "g fine p"
  25.111    by (metis assms box_real(2) fine_division_exists)
  25.112  
  25.113 -subsection \<open>A technical lemma about "refinement" of division.\<close>
  25.114 +subsection \<open>A technical lemma about "refinement" of division\<close>
  25.115  
  25.116  lemma tagged_division_finer:
  25.117    fixes p :: "('a::euclidean_space \<times> ('a::euclidean_space set)) set"
    26.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Apr 08 12:31:08 2018 +0200
    26.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Apr 09 16:20:23 2018 +0200
    26.3 @@ -4,7 +4,7 @@
    26.4      Author:     Brian Huffman, Portland State University
    26.5  *)
    26.6  
    26.7 -section \<open>Elementary topology in Euclidean space.\<close>
    26.8 +section \<open>Elementary topology in Euclidean space\<close>
    26.9  
   26.10  theory Topology_Euclidean_Space
   26.11  imports
   26.12 @@ -1873,7 +1873,7 @@
   26.13      by (auto simp: box_def inner_sum_left inner_Basis sum.If_cases)
   26.14  qed
   26.15  
   26.16 -subsection \<open>Intervals in general, including infinite and mixtures of open and closed.\<close>
   26.17 +subsection \<open>Intervals in general, including infinite and mixtures of open and closed\<close>
   26.18  
   26.19  definition%important "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
   26.20    (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
   26.21 @@ -5653,7 +5653,7 @@
   26.22      shows "closedin (subtopology euclidean S) (S \<inter> f -` T)"
   26.23  using assms continuous_on_closed by blast
   26.24  
   26.25 -subsection%unimportant \<open>Half-global and completely global cases.\<close>
   26.26 +subsection%unimportant \<open>Half-global and completely global cases\<close>
   26.27  
   26.28  lemma continuous_openin_preimage_gen:
   26.29    assumes "continuous_on S f"  "open T"
   26.30 @@ -5743,7 +5743,7 @@
   26.31    with \<open>x = f y\<close> show "x \<in> f ` interior S" ..
   26.32  qed
   26.33  
   26.34 -subsection%unimportant \<open>Topological properties of linear functions.\<close>
   26.35 +subsection%unimportant \<open>Topological properties of linear functions\<close>
   26.36  
   26.37  lemma linear_lim_0:
   26.38    assumes "bounded_linear f"