# HG changeset patch
# User nipkow
# Date 1523283623 -7200
# Node ID a5ad4c015d1c74b446e94819d4276d693036fe61
# Parent  5a4280946a256bf30da3d37804e6411846033f01
removed dots at the end of (sub)titles

diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Arcwise_Connected.thy
--- a/src/HOL/Analysis/Arcwise_Connected.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Arcwise_Connected.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -109,7 +109,7 @@
 
 subsection\<open>Arcwise Connections\<close>
 
-subsection\<open>Density of points with dyadic rational coordinates.\<close>
+subsection\<open>Density of points with dyadic rational coordinates\<close>
 
 proposition closure_dyadic_rationals:
     "closure (\<Union>k. \<Union>f \<in> Basis \<rightarrow> \<int>.
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -16,7 +16,7 @@
 (*              (c) Copyright, John Harrison 1998-2008                       *)
 (* ========================================================================= *)
 
-section \<open>Results connected with topological dimension.\<close>
+section \<open>Results connected with topological dimension\<close>
 
 theory Brouwer_Fixpoint
 imports Path_Connected Homeomorphism
@@ -117,7 +117,7 @@
 qed
 
 
-subsection \<open>The key "counting" observation, somewhat abstracted.\<close>
+subsection \<open>The key "counting" observation, somewhat abstracted\<close>
 
 lemma kuhn_counting_lemma:
   fixes bnd compo compo' face S F
@@ -148,7 +148,7 @@
     by auto
 qed
 
-subsection \<open>The odd/even result for faces of complete vertices, generalized.\<close>
+subsection \<open>The odd/even result for faces of complete vertices, generalized\<close>
 
 lemma kuhn_complete_lemma:
   assumes [simp]: "finite simplices"
@@ -2367,7 +2367,7 @@
 qed
 
 
-subsection\<open>Punctured affine hulls, etc.\<close>
+subsection\<open>Punctured affine hulls, etc\<close>
 
 lemma continuous_on_compact_surface_projection_aux:
   fixes S :: "'a::t2_space set"
@@ -2716,7 +2716,7 @@
     by blast
 qed
 
-subsection\<open>Absolute retracts, Etc.\<close>
+subsection\<open>Absolute retracts, etc\<close>
 
 text\<open>Absolute retracts (AR), absolute neighbourhood retracts (ANR) and also
  Euclidean neighbourhood retracts (ENR). We define AR and ANR by
@@ -3110,7 +3110,7 @@
   shows "S homeomorphic T \<Longrightarrow> ANR S \<longleftrightarrow> ANR T"
 by (metis ANR_homeomorphic_ANR homeomorphic_sym)
 
-subsection\<open> Analogous properties of ENRs.\<close>
+subsection\<open> Analogous properties of ENRs\<close>
 
 proposition ENR_imp_absolute_neighbourhood_retract:
   fixes S :: "'a::euclidean_space set" and S' :: "'b::euclidean_space set"
@@ -4274,7 +4274,7 @@
   shows "ANR c"
   by (metis ANR_connected_component_ANR assms componentsE)
 
-subsection\<open>Original ANR material, now for ENRs.\<close>
+subsection\<open>Original ANR material, now for ENRs\<close>
 
 lemma ENR_bounded:
   fixes S :: "'a::euclidean_space set"
@@ -4438,7 +4438,7 @@
   by (simp add: ENR_imp_ANR ENR_sphere)
 
 
-subsection\<open>Spheres are connected, etc.\<close>
+subsection\<open>Spheres are connected, etc\<close>
 
 lemma locally_path_connected_sphere_gen:
   fixes S :: "'a::euclidean_space set"
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -1,4 +1,4 @@
-section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space.\<close>
+section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space\<close>
 
 theory Cartesian_Euclidean_Space
 imports Finite_Cartesian_Product Derivative
@@ -21,7 +21,7 @@
   qed simp
 qed simp
 
-subsection\<open>Basic componentwise operations on vectors.\<close>
+subsection\<open>Basic componentwise operations on vectors\<close>
 
 instantiation vec :: (times, finite) times
 begin
@@ -93,7 +93,7 @@
   where "c *s x = (\<chi> i. c * (x$i))"
 
 
-subsection \<open>A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space.\<close>
+subsection \<open>A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space\<close>
 
 lemma sum_cong_aux:
   "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> sum f A = sum g A"
@@ -170,7 +170,7 @@
   vector_scaleR_component cond_component
 
 
-subsection \<open>Some frequently useful arithmetic lemmas over vectors.\<close>
+subsection \<open>Some frequently useful arithmetic lemmas over vectors\<close>
 
 instance vec :: (semigroup_mult, finite) semigroup_mult
   by standard (vector mult.assoc)
@@ -719,7 +719,7 @@
   done
 
 
-subsection\<open>Some bounds on components etc. relative to operator norm.\<close>
+subsection\<open>Some bounds on components etc. relative to operator norm\<close>
 
 lemma norm_column_le_onorm:
   fixes A :: "real^'n^'m"
@@ -1416,7 +1416,7 @@
 
 
 subsection \<open>Component of the differential must be zero if it exists at a local
-  maximum or minimum for that corresponding component.\<close>
+  maximum or minimum for that corresponding component\<close>
 
 lemma differential_zero_maxmin_cart:
   fixes f::"real^'a \<Rightarrow> real^'b"
@@ -1489,7 +1489,7 @@
 
 end
 
-subsection\<open>The collapse of the general concepts to dimension one.\<close>
+subsection\<open>The collapse of the general concepts to dimension one\<close>
 
 lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
   by (simp add: vec_eq_iff)
@@ -1510,7 +1510,7 @@
   by (auto simp add: norm_real dist_norm)
 
 
-subsection\<open>Explicit vector construction from lists.\<close>
+subsection\<open>Explicit vector construction from lists\<close>
 
 definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)"
 
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -3550,7 +3550,7 @@
   apply (force simp: algebra_simps)
   done
 
-subsubsection\<open>Some lemmas about negating a path.\<close>
+subsubsection\<open>Some lemmas about negating a path\<close>
 
 lemma valid_path_negatepath: "valid_path \<gamma> \<Longrightarrow> valid_path (uminus \<circ> \<gamma>)"
    unfolding o_def using piecewise_C1_differentiable_neg valid_path_def by blast
@@ -3965,7 +3965,7 @@
 qed
 
 
-subsection\<open>Continuity of winding number and invariance on connected sets.\<close>
+subsection\<open>Continuity of winding number and invariance on connected sets\<close>
 
 lemma continuous_at_winding_number:
   fixes z::complex
@@ -4436,7 +4436,7 @@
 qed
 
 
-subsection\<open>Cauchy's integral formula, again for a convex enclosing set.\<close>
+subsection\<open>Cauchy's integral formula, again for a convex enclosing set\<close>
 
 lemma Cauchy_integral_formula_weak:
     assumes s: "convex s" and "finite k" and conf: "continuous_on s f"
@@ -5374,7 +5374,7 @@
   using assms by (auto simp: vector_derivative_circlepath norm_mult intro!: contour_integral_uniform_limit)
 
 
-subsection\<open> General stepping result for derivative formulas.\<close>
+subsection\<open> General stepping result for derivative formulas\<close>
 
 proposition Cauchy_next_derivative:
   assumes "continuous_on (path_image \<gamma>) f'"
@@ -5614,7 +5614,7 @@
     by simp (rule fder)
 qed
 
-subsection\<open> Existence of all higher derivatives.\<close>
+subsection\<open>Existence of all higher derivatives\<close>
 
 proposition derivative_is_holomorphic:
   assumes "open s"
@@ -5699,7 +5699,7 @@
 qed
 
 
-subsection\<open> Morera's theorem.\<close>
+subsection\<open>Morera's theorem\<close>
 
 lemma Morera_local_triangle_ball:
   assumes "\<And>z. z \<in> s
@@ -5783,7 +5783,7 @@
 
 
 
-subsection\<open> Combining theorems for higher derivatives including Leibniz rule.\<close>
+subsection\<open>Combining theorems for higher derivatives including Leibniz rule\<close>
 
 lemma higher_deriv_linear [simp]:
     "(deriv ^^ n) (\<lambda>w. c*w) = (\<lambda>z. if n = 0 then c*z else if n = 1 then c else 0)"
@@ -6139,7 +6139,7 @@
   by (simp add: power2_eq_square)
 
 
-subsection\<open>A holomorphic function is analytic, i.e. has local power series.\<close>
+subsection\<open>A holomorphic function is analytic, i.e. has local power series\<close>
 
 theorem holomorphic_power_series:
   assumes holf: "f holomorphic_on ball z r"
@@ -6255,7 +6255,7 @@
 qed
 
 
-subsection\<open>The Liouville theorem and the Fundamental Theorem of Algebra.\<close>
+subsection\<open>The Liouville theorem and the Fundamental Theorem of Algebra\<close>
 
 text\<open> These weak Liouville versions don't even need the derivative formula.\<close>
 
@@ -6343,7 +6343,7 @@
 qed
 
 
-subsection\<open> Weierstrass convergence theorem.\<close>
+subsection\<open>Weierstrass convergence theorem\<close>
 
 proposition holomorphic_uniform_limit:
   assumes cont: "eventually (\<lambda>n. continuous_on (cball z r) (f n) \<and> (f n) holomorphic_on ball z r) F"
@@ -6490,7 +6490,7 @@
 qed
 
 
-subsection\<open>Some more simple/convenient versions for applications.\<close>
+subsection\<open>Some more simple/convenient versions for applications\<close>
 
 lemma holomorphic_uniform_sequence:
   assumes S: "open S"
@@ -6548,7 +6548,7 @@
 qed
 
 
-subsection\<open>On analytic functions defined by a series.\<close>
+subsection\<open>On analytic functions defined by a series\<close>
  
 lemma series_and_derivative_comparison:
   fixes S :: "complex set"
@@ -6767,7 +6767,7 @@
   by (simp add: analytic_on_open holomorphic_iff_power_series)
 
 
-subsection\<open>Equality between holomorphic functions, on open ball then connected set.\<close>
+subsection\<open>Equality between holomorphic functions, on open ball then connected set\<close>
 
 lemma holomorphic_fun_eq_on_ball:
    "\<lbrakk>f holomorphic_on ball z r; g holomorphic_on ball z r;
@@ -6846,7 +6846,7 @@
   done
 
 
-subsection\<open>Some basic lemmas about poles/singularities.\<close>
+subsection\<open>Some basic lemmas about poles/singularities\<close>
 
 lemma pole_lemma:
   assumes holf: "f holomorphic_on s" and a: "a \<in> interior s"
@@ -7002,7 +7002,7 @@
 qed
 
 
-subsection\<open>General, homology form of Cauchy's theorem.\<close>
+subsection\<open>General, homology form of Cauchy's theorem\<close>
 
 text\<open>Proof is based on Dixon's, as presented in Lang's "Complex Analysis" book (page 147).\<close>
 
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -174,7 +174,7 @@
   "(\<And>x. DERIV f x :> 0) \<Longrightarrow> f x = f a"
   by (metis DERIV_zero_unique UNIV_I convex_UNIV)
 
-subsection \<open>Some limit theorems about real part of real series etc.\<close>
+subsection \<open>Some limit theorems about real part of real series etc\<close>
 
 (*MOVE? But not to Finite_Cartesian_Product*)
 lemma sums_vec_nth :
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -77,7 +77,7 @@
   "f holomorphic_on s \<Longrightarrow> (\<lambda>x. exp (f x)) holomorphic_on s"
   using holomorphic_on_compose[OF _ holomorphic_on_exp] by (simp add: o_def)
 
-subsection\<open>Euler and de Moivre formulas.\<close>
+subsection\<open>Euler and de Moivre formulas\<close>
 
 text\<open>The sine series times @{term i}\<close>
 lemma sin_i_eq: "(\<lambda>n. (\<i> * sin_coeff n) * z^n) sums (\<i> * sin z)"
@@ -176,7 +176,7 @@
 lemma holomorphic_on_cos: "cos holomorphic_on s"
   by (simp add: field_differentiable_within_cos holomorphic_on_def)
 
-subsection\<open>Get a nice real/imaginary separation in Euler's formula.\<close>
+subsection\<open>Get a nice real/imaginary separation in Euler's formula\<close>
 
 lemma Euler: "exp(z) = of_real(exp(Re z)) *
               (of_real(cos(Im z)) + \<i> * of_real(sin(Im z)))"
@@ -626,7 +626,7 @@
 qed
 
 
-subsection\<open>Taylor series for complex exponential, sine and cosine.\<close>
+subsection\<open>Taylor series for complex exponential, sine and cosine\<close>
 
 declare power_Suc [simp del]
 
@@ -3503,7 +3503,7 @@
 lemma of_real_arccos: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
   by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0)
 
-subsection\<open>Some interrelationships among the real inverse trig functions.\<close>
+subsection\<open>Some interrelationships among the real inverse trig functions\<close>
 
 lemma arccos_arctan:
   assumes "-1 < x" "x < 1"
@@ -3573,7 +3573,7 @@
   using arccos_arcsin_sqrt_pos [of "-x"]
   by (simp add: arccos_minus)
 
-subsection\<open>continuity results for arcsin and arccos.\<close>
+subsection\<open>Continuity results for arcsin and arccos\<close>
 
 lemma continuous_on_Arcsin_real [continuous_intros]:
     "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arcsin"
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -1,4 +1,4 @@
-section \<open>Conformal Mappings. Consequences of Cauchy's integral theorem.\<close>
+section \<open>Conformal Mappings and Consequences of Cauchy's integral theorem\<close>
 
 text\<open>By John Harrison et al.  Ported from HOL Light by L C Paulson (2016)\<close>
 
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Connected.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -2,13 +2,13 @@
     Material split off from Topology_Euclidean_Space
 *)
 
-section \<open>Connected Components, Homeomorphisms, Baire property, etc.\<close>
+section \<open>Connected Components, Homeomorphisms, Baire property, etc\<close>
 
 theory Connected
 imports Topology_Euclidean_Space
 begin
 
-subsection%unimportant \<open>More properties of closed balls, spheres, etc.\<close>
+subsection%unimportant \<open>More properties of closed balls, spheres, etc\<close>
 
 lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
   apply (simp add: interior_def, safe)
@@ -961,7 +961,7 @@
   qed
 qed
 
-subsection%unimportant \<open>Some theorems on sups and infs using the notion "bounded".\<close>
+subsection%unimportant \<open>Some theorems on sups and infs using the notion "bounded"\<close>
 
 lemma bounded_real: "bounded (S::real set) \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. \<bar>x\<bar> \<le> a)"
   by (simp add: bounded_iff)
@@ -1139,7 +1139,7 @@
 qed
 
 
-subsection%unimportant\<open>Relations among convergence and absolute convergence for power series.\<close>
+subsection%unimportant\<open>Relations among convergence and absolute convergence for power series\<close>
 
 lemma summable_imp_bounded:
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
@@ -1515,7 +1515,7 @@
     by (simp add: compact_eq_bounded_closed)
 qed
 
-subsection%unimportant \<open>Equality of continuous functions on closure and related results.\<close>
+subsection%unimportant \<open>Equality of continuous functions on closure and related results\<close>
 
 lemma continuous_closedin_preimage_constant:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
@@ -2047,7 +2047,7 @@
   shows "bounded(f ` S)"
   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)
 
-subsection%unimportant \<open>Making a continuous function avoid some value in a neighbourhood.\<close>
+subsection%unimportant \<open>Making a continuous function avoid some value in a neighbourhood\<close>
 
 lemma continuous_within_avoid:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
@@ -2363,7 +2363,7 @@
     unfolding mem_interior using \<open>e > 0\<close> by auto
 qed
 
-subsection \<open>Continuity implies uniform continuity on a compact domain.\<close>
+subsection \<open>Continuity implies uniform continuity on a compact domain\<close>
 
 text\<open>From the proof of the Heine-Borel theorem: Lemma 2 in section 3.7, page 69 of
 J. C. Burkill and H. Burkill. A Second Course in Mathematical Analysis (CUP, 2002)\<close>
@@ -2666,7 +2666,7 @@
 qed
 
 
-subsection \<open>The diameter of a set.\<close>
+subsection \<open>The diameter of a set\<close>
 
 definition%important diameter :: "'a::metric_space set \<Rightarrow> real" where
   "diameter S = (if S = {} then 0 else SUP (x,y):S\<times>S. dist x y)"
@@ -3014,7 +3014,7 @@
 qed
 
 
-subsection%unimportant \<open>Compact sets and the closure operation.\<close>
+subsection%unimportant \<open>Compact sets and the closure operation\<close>
 
 lemma closed_scaling:
   fixes S :: "'a::real_normed_vector set"
@@ -3321,7 +3321,7 @@
 using assms
 by (auto simp: continuous_on_id intro: continuous_on_cases_le [where h = id, simplified])
 
-subsubsection\<open>Some more convenient intermediate-value theorem formulations.\<close>
+subsubsection\<open>Some more convenient intermediate-value theorem formulations\<close>
 
 lemma connected_ivt_hyperplane:
   assumes "connected S" and xy: "x \<in> S" "y \<in> S" and b: "inner a x \<le> b" "b \<le> inner a y"
@@ -3901,7 +3901,7 @@
 qed
 
 
-subsection \<open>"Isometry" (up to constant bounds) of injective linear map etc.\<close>
+subsection \<open>"Isometry" (up to constant bounds) of injective linear map etc\<close>
 
 lemma cauchy_isometric:
   assumes e: "e > 0"
@@ -4976,7 +4976,7 @@
 
 
 
-subsection\<open>A couple of lemmas about components (see Newman IV, 3.3 and 3.4).\<close>
+subsection\<open>A couple of lemmas about components (see Newman IV, 3.3 and 3.4)\<close>
 
 
 lemma connected_Un_clopen_in_complement:
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Continuous_Extension.thy
--- a/src/HOL/Analysis/Continuous_Extension.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Continuous_Extension.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -295,7 +295,7 @@
 using%unimportant assms by (auto intro: Urysohn_local [of UNIV S T a b])
 
 
-subsection\<open> The Dugundji extension theorem, and Tietze variants as corollaries.\<close>
+subsection\<open>The Dugundji extension theorem and Tietze variants as corollaries\<close>
 
 text%important\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
 http://projecteuclid.org/euclid.pjm/1103052106\<close>
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Continuum_Not_Denumerable.thy
--- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -3,7 +3,7 @@
     Author:     Johannes Hölzl, TU München
 *)
 
-section \<open>Non-denumerability of the Continuum.\<close>
+section \<open>Non-denumerability of the Continuum\<close>
 
 theory Continuum_Not_Denumerable
 imports
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -4283,7 +4283,7 @@
 by (metis low_dim_interior)
 
 
-subsection \<open>Caratheodory's theorem.\<close>
+subsection \<open>Caratheodory's theorem\<close>
 
 lemma convex_hull_caratheodory_aff_dim:
   fixes p :: "('a::euclidean_space) set"
@@ -5151,7 +5151,7 @@
   by (metis Int_absorb1 Int_absorb2 convex_hull_subset_affine_hull hull_hull hull_mono hull_subset)
 
 
-subsection%unimportant \<open>Openness and compactness are preserved by convex hull operation.\<close>
+subsection%unimportant \<open>Openness and compactness are preserved by convex hull operation\<close>
 
 lemma open_convex_hull[intro]:
   fixes s :: "'a::real_normed_vector set"
@@ -5422,7 +5422,7 @@
 qed
 
 
-subsection%unimportant \<open>Extremal points of a simplex are some vertices.\<close>
+subsection%unimportant \<open>Extremal points of a simplex are some vertices\<close>
 
 lemma dist_increases_online:
   fixes a b d :: "'a::real_inner"
@@ -5621,7 +5621,7 @@
   by(cases "s = {}") auto
 
 
-subsection \<open>Closest point of a convex set is unique, with a continuous projection.\<close>
+subsection \<open>Closest point of a convex set is unique, with a continuous projection\<close>
 
 definition%important closest_point :: "'a::{real_inner,heine_borel} set \<Rightarrow> 'a \<Rightarrow> 'a"
   where "closest_point s a = (SOME x. x \<in> s \<and> (\<forall>y\<in>s. dist a x \<le> dist a y))"
@@ -5811,7 +5811,7 @@
 qed
 
 
-subsubsection%unimportant \<open>Various point-to-set separating/supporting hyperplane theorems.\<close>
+subsubsection%unimportant \<open>Various point-to-set separating/supporting hyperplane theorems\<close>
 
 lemma supporting_hyperplane_closed_point:
   fixes z :: "'a::{real_inner,heine_borel}"
@@ -6132,7 +6132,7 @@
   using hull_subset[of s convex] convex_hull_empty by auto
 
 
-subsection%unimportant \<open>Moving and scaling convex hulls.\<close>
+subsection%unimportant \<open>Moving and scaling convex hulls\<close>
 
 lemma convex_hull_set_plus:
   "convex hull (s + t) = convex hull s + convex hull t"
@@ -6657,7 +6657,7 @@
      "\<lbrakk>connected S; aff_dim S \<noteq> 0; a \<in> S\<rbrakk> \<Longrightarrow> a islimpt S"
   using aff_dim_sing connected_imp_perfect by blast
 
-subsection%unimportant \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close>
+subsection%unimportant \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent\<close>
 
 lemma mem_is_interval_1_I:
   fixes a b c::real
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -15,7 +15,7 @@
 
 subsection \<open>Derivatives\<close>
 
-subsubsection \<open>Combining theorems.\<close>
+subsubsection \<open>Combining theorems\<close>
 
 lemmas has_derivative_id = has_derivative_ident
 lemmas has_derivative_neg = has_derivative_minus
@@ -32,7 +32,7 @@
   by (intro derivative_eq_intros) auto
 
 
-subsection \<open>Derivative with composed bilinear function.\<close>
+subsection \<open>Derivative with composed bilinear function\<close>
 
 lemma has_derivative_bilinear_within:
   assumes "(f has_derivative f') (at x within s)"
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Determinants.thy
--- a/src/HOL/Analysis/Determinants.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Determinants.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -929,7 +929,7 @@
     by auto
 qed
 
-subsection \<open>Orthogonality of a transformation and matrix.\<close>
+subsection \<open>Orthogonality of a transformation and matrix\<close>
 
 definition "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
 
@@ -1087,7 +1087,7 @@
   using det_orthogonal_matrix orthogonal_transformation_matrix by fastforce
 
 
-subsection \<open>Linearity of scaling, and hence isometry, that preserves origin.\<close>
+subsection \<open>Linearity of scaling, and hence isometry, that preserves origin\<close>
 
 lemma scaling_linear:
   fixes f :: "'a::real_inner \<Rightarrow> 'a::real_inner"
@@ -1157,7 +1157,7 @@
     by (auto simp: orthogonal_transformation_isometry)
 qed
 
-subsection\<open> We can find an orthogonal matrix taking any unit vector to any other.\<close>
+subsection\<open> We can find an orthogonal matrix taking any unit vector to any other\<close>
 
 lemma orthogonal_matrix_transpose [simp]:
      "orthogonal_matrix(transpose A) \<longleftrightarrow> orthogonal_matrix A"
@@ -1251,7 +1251,7 @@
 qed
 
 
-subsection \<open>Can extend an isometry from unit sphere.\<close>
+subsection \<open>Can extend an isometry from unit sphere\<close>
 
 lemma isometry_sphere_extend:
   fixes f:: "'a::real_inner \<Rightarrow> 'a"
@@ -1349,7 +1349,7 @@
     done
 qed
 
-subsection \<open>Rotation, reflection, rotoinversion.\<close>
+subsection \<open>Rotation, reflection, rotoinversion\<close>
 
 definition "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
 definition "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Fashoda_Theorem.thy
--- a/src/HOL/Analysis/Fashoda_Theorem.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -8,7 +8,7 @@
 imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
 begin
 
-subsection \<open>Bijections between intervals.\<close>
+subsection \<open>Bijections between intervals\<close>
 
 definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
   where "interval_bij =
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -2,7 +2,7 @@
     Author:     Amine Chaieb, University of Cambridge
 *)
 
-section \<open>Definition of finite Cartesian product types.\<close>
+section \<open>Definition of finite Cartesian product types\<close>
 
 theory Finite_Cartesian_Product
 imports
@@ -13,7 +13,7 @@
   "HOL-Library.FuncSet"
 begin
 
-subsection \<open>Finite Cartesian products, with indexing and lambdas.\<close>
+subsection \<open>Finite Cartesian products, with indexing and lambdas\<close>
 
 typedef ('a, 'b) vec = "UNIV :: ('b::finite \<Rightarrow> 'a) set"
   morphisms vec_nth vec_lambda ..
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -1,4 +1,4 @@
-section \<open>Extending Continous Maps, Invariance of Domain, etc..\<close>
+section \<open>Extending Continous Maps, Invariance of Domain, etc\<close>
 
 text\<open>Ported from HOL Light (moretop.ml) by L C Paulson\<close>
 
@@ -367,7 +367,7 @@
 
 
 
-subsection\<open> Some technical lemmas about extending maps from cell complexes.\<close>
+subsection\<open> Some technical lemmas about extending maps from cell complexes\<close>
 
 lemma extending_maps_Union_aux:
   assumes fin: "finite \<F>"
@@ -981,7 +981,7 @@
 
 
 
-subsection\<open> Special cases and corollaries involving spheres.\<close>
+subsection\<open> Special cases and corollaries involving spheres\<close>
 
 lemma disjnt_Diff1: "X \<subseteq> Y' \<Longrightarrow> disjnt (X - Y) (X' - Y')"
   by (auto simp: disjnt_def)
@@ -2727,7 +2727,7 @@
     using clopen [of S] False  by simp
 qed
 
-subsection\<open> Dimension-based conditions for various homeomorphisms.\<close>
+subsection\<open>Dimension-based conditions for various homeomorphisms\<close>
 
 lemma homeomorphic_subspaces_eq:
   fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
@@ -3896,7 +3896,7 @@
 qed
 
 
-subsection\<open>Another simple case where sphere maps are nullhomotopic.\<close>
+subsection\<open>Another simple case where sphere maps are nullhomotopic\<close>
 
 lemma inessential_spheremap_2_aux:
   fixes f :: "'a::euclidean_space \<Rightarrow> complex"
@@ -3962,7 +3962,7 @@
 qed
 
 
-subsection\<open>Holomorphic logarithms and square roots.\<close>
+subsection\<open>Holomorphic logarithms and square roots\<close>
 
 lemma contractible_imp_holomorphic_log:
   assumes holf: "f holomorphic_on S"
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -3,7 +3,7 @@
                 Huge cleanup by LCP
 *)
 
-section \<open>Henstock-Kurzweil gauge integration in many dimensions.\<close>
+section \<open>Henstock-Kurzweil gauge integration in many dimensions\<close>
 
 theory Henstock_Kurzweil_Integration
 imports
@@ -28,7 +28,7 @@
   by blast
 (* END MOVE *)
 
-subsection \<open>Content (length, area, volume...) of an interval.\<close>
+subsection \<open>Content (length, area, volume...) of an interval\<close>
 
 abbreviation content :: "'a::euclidean_space set \<Rightarrow> real"
   where "content s \<equiv> measure lborel s"
@@ -313,7 +313,7 @@
 lemma has_integral_integral: "f integrable_on s \<longleftrightarrow> (f has_integral (integral s f)) s"
   by auto
 
-subsection \<open>Basic theorems about integrals.\<close>
+subsection \<open>Basic theorems about integrals\<close>
 
 lemma has_integral_eq_rhs: "(f has_integral j) S \<Longrightarrow> i = j \<Longrightarrow> (f has_integral i) S"
   by (rule forw_subst)
@@ -909,7 +909,7 @@
 
 
 
-subsection \<open>Cauchy-type criterion for integrability.\<close>
+subsection \<open>Cauchy-type criterion for integrability\<close>
 
 proposition integrable_Cauchy:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::{real_normed_vector,complete_space}"
@@ -1012,7 +1012,7 @@
 qed
 
 
-subsection \<open>Additivity of integral on abutting intervals.\<close>
+subsection \<open>Additivity of integral on abutting intervals\<close>
 
 lemma tagged_division_split_left_inj_content:
   assumes \<D>: "\<D> tagged_division_of S"
@@ -1261,7 +1261,7 @@
 qed
 
 
-subsection \<open>A sort of converse, integrability on subintervals.\<close>
+subsection \<open>A sort of converse, integrability on subintervals\<close>
 
 lemma has_integral_separate_sides:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
@@ -1459,7 +1459,7 @@
   qed
 qed
 
-subsection \<open>Bounds on the norm of Riemann sums and the integral itself.\<close>
+subsection \<open>Bounds on the norm of Riemann sums and the integral itself\<close>
 
 lemma dsum_bound:
   assumes "p division_of (cbox a b)"
@@ -1562,7 +1562,7 @@
 by (metis integrable_integral has_integral_bound assms)
 
 
-subsection \<open>Similar theorems about relationship among components.\<close>
+subsection \<open>Similar theorems about relationship among components\<close>
 
 lemma rsum_component_le:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -1764,7 +1764,7 @@
   using assms
   by (metis box_real(2) integral_component_ubound)
 
-subsection \<open>Uniform limit of integrable functions is integrable.\<close>
+subsection \<open>Uniform limit of integrable functions is integrable\<close>
 
 lemma real_arch_invD:
   "0 < (e::real) \<Longrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
@@ -1907,13 +1907,13 @@
 lemmas integrable_uniform_limit_real = integrable_uniform_limit [where 'a=real, simplified]
 
 
-subsection \<open>Negligible sets.\<close>
+subsection \<open>Negligible sets\<close>
 
 definition "negligible (s:: 'a::euclidean_space set) \<longleftrightarrow>
   (\<forall>a b. ((indicator s :: 'a\<Rightarrow>real) has_integral 0) (cbox a b))"
 
 
-subsubsection \<open>Negligibility of hyperplane.\<close>
+subsubsection \<open>Negligibility of hyperplane\<close>
 
 lemma content_doublesplit:
   fixes a :: "'a::euclidean_space"
@@ -2082,7 +2082,7 @@
 qed
 
 
-subsubsection \<open>Hence the main theorem about negligible sets.\<close>
+subsubsection \<open>Hence the main theorem about negligible sets\<close>
 
 
 lemma has_integral_negligible_cbox:
@@ -2276,7 +2276,7 @@
     by (auto simp: integral_def integrable_on_def)
 
 
-subsection \<open>Some other trivialities about negligible sets.\<close>
+subsection \<open>Some other trivialities about negligible sets\<close>
 
 lemma negligible_subset:
   assumes "negligible s" "t \<subseteq> s"
@@ -2366,7 +2366,7 @@
 qed auto
 
 
-subsection \<open>Finite case of the spike theorem is quite commonly needed.\<close>
+subsection \<open>Finite case of the spike theorem is quite commonly needed\<close>
 
 lemma has_integral_spike_finite:
   assumes "finite S"
@@ -2414,7 +2414,7 @@
   by (metis assms box_real(2) has_integral_bound_spike_finite)
 
 
-subsection \<open>In particular, the boundary of an interval is negligible.\<close>
+subsection \<open>In particular, the boundary of an interval is negligible\<close>
 
 lemma negligible_frontier_interval: "negligible(cbox (a::'a::euclidean_space) b - box a b)"
 proof -
@@ -2445,7 +2445,7 @@
   using assms has_integral_spike_interior_eq by blast
 
 
-subsection \<open>Integrability of continuous functions.\<close>
+subsection \<open>Integrability of continuous functions\<close>
 
 lemma operative_approximableI:
   fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
@@ -2573,10 +2573,10 @@
   by (auto intro!: integrable_continuous_interval simp: closed_segment_eq_real_ivl)
 
 
-subsection \<open>Specialization of additivity to one dimension.\<close>
-
-
-subsection \<open>A useful lemma allowing us to factor out the content size.\<close>
+subsection \<open>Specialization of additivity to one dimension\<close>
+
+
+subsection \<open>A useful lemma allowing us to factor out the content size\<close>
 
 lemma has_integral_factor_content:
   "(f has_integral i) (cbox a b) \<longleftrightarrow>
@@ -2642,7 +2642,7 @@
   by (rule has_integral_factor_content)
 
 
-subsection \<open>Fundamental theorem of calculus.\<close>
+subsection \<open>Fundamental theorem of calculus\<close>
 
 lemma interval_bounds_real:
   fixes q b :: real
@@ -2884,7 +2884,7 @@
 qed
 
 
-subsection \<open>Only need trivial subintervals if the interval itself is trivial.\<close>
+subsection \<open>Only need trivial subintervals if the interval itself is trivial\<close>
 
 proposition division_of_nontrivial:
   fixes \<D> :: "'a::euclidean_space set set"
@@ -2970,7 +2970,7 @@
 qed
 
 
-subsection \<open>Integrability on subintervals.\<close>
+subsection \<open>Integrability on subintervals\<close>
 
 lemma operative_integrableI:
   fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
@@ -3016,7 +3016,7 @@
   shows "f integrable_on {c..d}"
   by (metis assms box_real(2) integrable_subinterval)
 
-subsection \<open>Combining adjacent intervals in 1 dimension.\<close>
+subsection \<open>Combining adjacent intervals in 1 dimension\<close>
 
 lemma has_integral_combine:
   fixes a b c :: real and j :: "'a::banach"
@@ -3087,7 +3087,7 @@
   using integral_combine[of b a c f] integral_combine[of a b c f]
   by (auto simp: algebra_simps min_def)
 
-subsection \<open>Reduce integrability to "local" integrability.\<close>
+subsection \<open>Reduce integrability to "local" integrability\<close>
 
 lemma integrable_on_little_subintervals:
   fixes f :: "'b::euclidean_space \<Rightarrow> 'a::banach"
@@ -3116,7 +3116,7 @@
 qed
 
 
-subsection \<open>Second FTC or existence of antiderivative.\<close>
+subsection \<open>Second FTC or existence of antiderivative\<close>
 
 lemma integrable_const[intro]: "(\<lambda>x. c) integrable_on cbox a b"
   unfolding integrable_on_def by blast
@@ -3204,7 +3204,7 @@
   obtains g where "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative (f x::_::banach)) (at x within {a..b})"
   using integral_has_vector_derivative[OF assms] by auto
 
-subsection \<open>Combined fundamental theorem of calculus.\<close>
+subsection \<open>Combined fundamental theorem of calculus\<close>
 
 lemma antiderivative_integral_continuous:
   fixes f :: "real \<Rightarrow> 'a::banach"
@@ -3227,7 +3227,7 @@
 qed
 
 
-subsection \<open>General "twiddling" for interval-to-interval function image.\<close>
+subsection \<open>General "twiddling" for interval-to-interval function image\<close>
 
 lemma has_integral_twiddle:
   assumes "0 < r"
@@ -3334,7 +3334,7 @@
 qed
 
 
-subsection \<open>Special case of a basic affine transformation.\<close>
+subsection \<open>Special case of a basic affine transformation\<close>
 
 lemma AE_lborel_inner_neq:
   assumes k: "k \<in> Basis"
@@ -3460,7 +3460,7 @@
 
 lemmas has_integral_affinity01 = has_integral_affinity [of _ _ 0 "1::real", simplified]
 
-subsection \<open>Special case of stretching coordinate axes separately.\<close>
+subsection \<open>Special case of stretching coordinate axes separately\<close>
 
 lemma has_integral_stretch:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
@@ -3485,7 +3485,7 @@
   by (force dest: has_integral_stretch)
 
 
-subsection \<open>even more special cases.\<close>
+subsection \<open>even more special cases\<close>
 
 lemma uminus_interval_vector[simp]:
   fixes a b :: "'a::euclidean_space"
@@ -3528,7 +3528,7 @@
   by (rule integral_reflect)
 
 
-subsection \<open>Stronger form of FCT; quite a tedious proof.\<close>
+subsection \<open>Stronger form of FCT; quite a tedious proof\<close>
 
 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"
   by (simp add: split_def)
@@ -3904,7 +3904,7 @@
 qed
 
 
-subsection \<open>Stronger form with finite number of exceptional points.\<close>
+subsection \<open>Stronger form with finite number of exceptional points\<close>
 
 lemma fundamental_theorem_of_calculus_interior_strong:
   fixes f :: "real \<Rightarrow> 'a::banach"
@@ -4217,7 +4217,7 @@
   by (auto simp: has_field_derivative_iff_has_vector_derivative)
 
 
-subsection \<open>This doesn't directly involve integration, but that gives an easy proof.\<close>
+subsection \<open>This doesn't directly involve integration, but that gives an easy proof\<close>
 
 lemma has_derivative_zero_unique_strong_interval:
   fixes f :: "real \<Rightarrow> 'a::banach"
@@ -4251,7 +4251,7 @@
 qed
 
 
-subsection \<open>Generalize a bit to any convex set.\<close>
+subsection \<open>Generalize a bit to any convex set\<close>
 
 lemma has_derivative_zero_unique_strong_convex:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
@@ -4919,7 +4919,7 @@
 qed
 
 
-subsection \<open>Continuity of the integral (for a 1-dimensional interval).\<close>
+subsection \<open>Continuity of the integral (for a 1-dimensional interval)\<close>
 
 lemma integrable_alt:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Jordan_Curve.thy
--- a/src/HOL/Analysis/Jordan_Curve.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Jordan_Curve.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -9,7 +9,7 @@
 
 begin
 
-subsection\<open>Janiszewski's theorem.\<close>
+subsection\<open>Janiszewski's theorem\<close>
 
 lemma Janiszewski_weak:
   fixes a b::complex
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -978,7 +978,8 @@
   then show ?thesis
     by (auto dest!: AE_not_in)
 qed
-subsection\<open> A nice lemma for negligibility proofs.\<close>
+
+subsection \<open>A nice lemma for negligibility proofs\<close>
 
 lemma summable_iff_suminf_neq_top: "(\<And>n. f n \<ge> 0) \<Longrightarrow> \<not> summable f \<Longrightarrow> (\<Sum>i. ennreal (f i)) = top"
   by (metis summable_suminf_not_top)
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -3380,7 +3380,7 @@
       by (metis dw_le norm_minus_commute not_less order_trans rle wy)
 qed
 
-section\<open> Homotopy of maps p,q : X=>Y with property P of all intermediate maps.\<close>
+section\<open> Homotopy of maps p,q : X=>Y with property P of all intermediate maps\<close>
 
 text%important\<open> We often just want to require that it fixes some subset, but to take in
   the case of a loop homotopy, it's convenient to have a general property P.\<close>
@@ -3487,7 +3487,7 @@
 qed
 
 
-subsection%unimportant\<open> Trivial properties.\<close>
+subsection%unimportant\<open>Trivial properties\<close>
 
 lemma homotopic_with_imp_property: "homotopic_with P X Y f g \<Longrightarrow> P f \<and> P g"
   unfolding homotopic_with_def Ball_def
@@ -3742,7 +3742,7 @@
 qed
 
 
-subsection\<open>Homotopy of paths, maintaining the same endpoints.\<close>
+subsection\<open>Homotopy of paths, maintaining the same endpoints\<close>
 
 
 definition%important homotopic_paths :: "['a set, real \<Rightarrow> 'a, real \<Rightarrow> 'a::topological_space] \<Rightarrow> bool"
@@ -3958,7 +3958,7 @@
 using%unimportant homotopic_paths_rinv [of "reversepath p" s] assms by simp
 
 
-subsection\<open> Homotopy of loops without requiring preservation of endpoints.\<close>
+subsection\<open>Homotopy of loops without requiring preservation of endpoints\<close>
 
 definition%important homotopic_loops :: "'a::topological_space set \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> bool"  where
  "homotopic_loops s p q \<equiv>
@@ -4197,7 +4197,7 @@
 qed
 
 
-subsection%unimportant\<open> Homotopy of "nearby" function, paths and loops.\<close>
+subsection%unimportant\<open>Homotopy of "nearby" function, paths and loops\<close>
 
 lemma homotopic_with_linear:
   fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
@@ -5521,7 +5521,7 @@
     by (metis open_openin openin_topspace subtopology_superset top.extremum topspace_euclidean_subtopology)
 qed
 
-subsection\<open>Sura-Bura's results about compact components of sets.\<close>
+subsection\<open>Sura-Bura's results about compact components of sets\<close>
 
 proposition Sura_Bura_compact:
   fixes S :: "'a::euclidean_space set"
@@ -7452,7 +7452,7 @@
 
 
 
-subsection\<open> Self-homeomorphisms shuffling points about in various ways.\<close>
+subsection\<open>Self-homeomorphisms shuffling points about in various ways\<close>
 
 subsubsection%unimportant\<open>The theorem \<open>homeomorphism_moving_points_exists\<close>\<close>
 
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Poly_Roots.thy
--- a/src/HOL/Analysis/Poly_Roots.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Poly_Roots.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -8,7 +8,7 @@
 imports Complex_Main
 begin
 
-subsection\<open>Basics about polynomial functions: extremal behaviour and root counts.\<close>
+subsection\<open>Basics about polynomial functions: extremal behaviour and root counts\<close>
 
 lemma sub_polyfun:
   fixes x :: "'a::{comm_ring,monoid_mult}"
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Polytope.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -1,4 +1,4 @@
-section \<open>Faces, Extreme Points, Polytopes, Polyhedra etc.\<close>
+section \<open>Faces, Extreme Points, Polytopes, Polyhedra etc\<close>
 
 text\<open>Ported from HOL Light by L C Paulson\<close>
 
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Riemann_Mapping.thy
--- a/src/HOL/Analysis/Riemann_Mapping.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Riemann_Mapping.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -8,7 +8,7 @@
 imports Great_Picard
 begin
 
-subsection\<open>Moebius functions are biholomorphisms of the unit disc.\<close>
+subsection\<open>Moebius functions are biholomorphisms of the unit disc\<close>
 
 definition Moebius_function :: "[real,complex,complex] \<Rightarrow> complex" where
   "Moebius_function \<equiv> \<lambda>t w z. exp(\<i> * of_real t) * (z - w) / (1 - cnj w * z)"
@@ -853,7 +853,7 @@
   using convex_imp_contractible homeomorphic_contractible_eq simply_connected_eq_homeomorphic_to_disc by auto
 
 
-subsection\<open>A further chain of equivalences about components of the complement of a simply connected set.\<close>
+subsection\<open>A further chain of equivalences about components of the complement of a simply connected set\<close>
 
 text\<open>(following 1.35 in Burckel'S book)\<close>
 
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Starlike.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -6,7 +6,7 @@
    Author:     Johannes Hoelzl, TU Muenchen
 *)
 
-section \<open>Line segments, Starlike Sets, etc.\<close>
+section \<open>Line segments, Starlike Sets, etc\<close>
 
 theory Starlike
   imports Convex_Euclidean_Space
@@ -4157,7 +4157,7 @@
     by (metis Diff_cancel convex_hull_singleton insert_absorb2 open_segment_def segment_convex_hull)
 qed
 
-subsection%unimportant\<open>Similar results for closure and (relative or absolute) frontier.\<close>
+subsection%unimportant\<open>Similar results for closure and (relative or absolute) frontier\<close>
 
 lemma closure_convex_hull [simp]:
   fixes s :: "'a::euclidean_space set"
@@ -7119,7 +7119,7 @@
   done
 qed
 
-subsection\<open>Decomposing a vector into parts in orthogonal subspaces.\<close>
+subsection\<open>Decomposing a vector into parts in orthogonal subspaces\<close>
 
 text\<open>existence of orthonormal basis for a subspace.\<close>
 
@@ -7470,7 +7470,7 @@
   finally show "dim T \<le> dim S" by simp
 qed
 
-subsection\<open>Lower-dimensional affine subsets are nowhere dense.\<close>
+subsection\<open>Lower-dimensional affine subsets are nowhere dense\<close>
 
 proposition%important dense_complement_subspace:
   fixes S :: "'a :: euclidean_space set"
@@ -7583,7 +7583,7 @@
   by (simp add: assms dense_complement_convex)
 
 
-subsection%unimportant\<open>Parallel slices, etc.\<close>
+subsection%unimportant\<open>Parallel slices, etc\<close>
 
 text\<open> If we take a slice out of a set, we can do it perpendicularly,
   with the normal vector to the slice parallel to the affine hull.\<close>
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Tagged_Division.thy
--- a/src/HOL/Analysis/Tagged_Division.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -55,7 +55,7 @@
     by (simp add: field_simps)
 qed
 
-subsection \<open>Some useful lemmas about intervals.\<close>
+subsection \<open>Some useful lemmas about intervals\<close>
 
 lemma interior_subset_union_intervals:
   assumes "i = cbox a b"
@@ -130,7 +130,7 @@
 lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
   by (simp add: box_ne_empty)
 
-subsection \<open>Bounds on intervals where they exist.\<close>
+subsection \<open>Bounds on intervals where they exist\<close>
 
 definition interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
   where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
@@ -192,7 +192,7 @@
       by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
 qed
 
-subsection \<open>The notion of a gauge --- simply an open set containing the point.\<close>
+subsection \<open>The notion of a gauge --- simply an open set containing the point\<close>
 
 definition "gauge \<gamma> \<longleftrightarrow> (\<forall>x. x \<in> \<gamma> x \<and> open (\<gamma> x))"
 
@@ -242,14 +242,14 @@
   "(\<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)"
   by (metis zero_less_one)
 
-subsection \<open>Attempt a systematic general set of "offset" results for components.\<close>
+subsection \<open>Attempt a systematic general set of "offset" results for components\<close>
 
 lemma gauge_modify:
   assumes "(\<forall>S. open S \<longrightarrow> open {x. f(x) \<in> S})" "gauge d"
   shows "gauge (\<lambda>x. {y. f y \<in> d (f x)})"
   using assms unfolding gauge_def by force
 
-subsection \<open>Divisions.\<close>
+subsection \<open>Divisions\<close>
 
 definition division_of (infixl "division'_of" 40)
 where
@@ -995,7 +995,7 @@
   }
 qed
 
-subsection \<open>Tagged (partial) divisions.\<close>
+subsection \<open>Tagged (partial) divisions\<close>
 
 definition tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40)
   where "s tagged_partial_division_of i \<longleftrightarrow>
@@ -1828,7 +1828,7 @@
 qed
 
 
-subsection \<open>Special case of additivity we need for the FTC.\<close>
+subsection \<open>Special case of additivity we need for the FTC\<close>
 
 lemma additive_tagged_division_1:
   fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
@@ -1856,7 +1856,7 @@
 qed
 
 
-subsection \<open>Fine-ness of a partition w.r.t. a gauge.\<close>
+subsection \<open>Fine-ness of a partition w.r.t. a gauge\<close>
 
 definition fine  (infixr "fine" 46)
   where "d fine s \<longleftrightarrow> (\<forall>(x,k) \<in> s. k \<subseteq> d x)"
@@ -1887,7 +1887,7 @@
 lemma fine_subset: "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p"
   unfolding fine_def by blast
 
-subsection \<open>Some basic combining lemmas.\<close>
+subsection \<open>Some basic combining lemmas\<close>
 
 lemma tagged_division_Union_exists:
   assumes "finite I"
@@ -1907,14 +1907,14 @@
 qed
 
 
-subsection \<open>The set we're concerned with must be closed.\<close>
+subsection \<open>The set we're concerned with must be closed\<close>
 
 lemma division_of_closed:
   fixes i :: "'n::euclidean_space set"
   shows "s division_of i \<Longrightarrow> closed i"
   unfolding division_of_def by fastforce
 
-subsection \<open>General bisection principle for intervals; might be useful elsewhere.\<close>
+subsection \<open>General bisection principle for intervals; might be useful elsewhere\<close>
 
 lemma interval_bisection_step:
   fixes type :: "'a::euclidean_space"
@@ -2185,7 +2185,7 @@
 qed
 
 
-subsection \<open>Cousin's lemma.\<close>
+subsection \<open>Cousin's lemma\<close>
 
 lemma fine_division_exists:
   fixes a b :: "'a::euclidean_space"
@@ -2231,7 +2231,7 @@
   obtains p where "p tagged_division_of {a .. b}" "g fine p"
   by (metis assms box_real(2) fine_division_exists)
 
-subsection \<open>A technical lemma about "refinement" of division.\<close>
+subsection \<open>A technical lemma about "refinement" of division\<close>
 
 lemma tagged_division_finer:
   fixes p :: "('a::euclidean_space \<times> ('a::euclidean_space set)) set"
diff -r 5a4280946a25 -r a5ad4c015d1c src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Apr 09 16:20:23 2018 +0200
@@ -4,7 +4,7 @@
     Author:     Brian Huffman, Portland State University
 *)
 
-section \<open>Elementary topology in Euclidean space.\<close>
+section \<open>Elementary topology in Euclidean space\<close>
 
 theory Topology_Euclidean_Space
 imports
@@ -1873,7 +1873,7 @@
     by (auto simp: box_def inner_sum_left inner_Basis sum.If_cases)
 qed
 
-subsection \<open>Intervals in general, including infinite and mixtures of open and closed.\<close>
+subsection \<open>Intervals in general, including infinite and mixtures of open and closed\<close>
 
 definition%important "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
   (\<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)"
@@ -5653,7 +5653,7 @@
     shows "closedin (subtopology euclidean S) (S \<inter> f -` T)"
 using assms continuous_on_closed by blast
 
-subsection%unimportant \<open>Half-global and completely global cases.\<close>
+subsection%unimportant \<open>Half-global and completely global cases\<close>
 
 lemma continuous_openin_preimage_gen:
   assumes "continuous_on S f"  "open T"
@@ -5743,7 +5743,7 @@
   with \<open>x = f y\<close> show "x \<in> f ` interior S" ..
 qed
 
-subsection%unimportant \<open>Topological properties of linear functions.\<close>
+subsection%unimportant \<open>Topological properties of linear functions\<close>
 
 lemma linear_lim_0:
   assumes "bounded_linear f"