diff -r f9bf65d90b69 -r 58a77f548bb6 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Thu Dec 27 19:48:41 2018 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Thu Dec 27 22:54:17 2018 +0100
@@ -132,6 +132,7 @@
   using assms inj_on_eq_iff [of f]
   by (auto simp: arc_def inj_on_def path_linear_image_eq)
 
+
 subsection%unimportant\<open>Basic lemmas about paths\<close>
 
 lemma continuous_on_path: "path f \<Longrightarrow> t \<subseteq> {0..1} \<Longrightarrow> continuous_on t f"
@@ -293,6 +294,7 @@
     done
 qed
 
+
 section%unimportant \<open>Path Images\<close>
 
 lemma bounded_path_image: "path g \<Longrightarrow> bounded(path_image g)"
@@ -937,6 +939,7 @@
 lemma join_subpaths_middle: "subpath (0) ((1 / 2)) p +++ subpath ((1 / 2)) 1 p = p"
   by (rule ext) (simp add: joinpaths_def subpath_def divide_simps)
 
+
 subsection%unimportant\<open>There is a subpath to the frontier\<close>
 
 lemma subpath_to_frontier_explicit:
@@ -1053,7 +1056,8 @@
     done
 qed
 
-subsection \<open>shiftpath: Reparametrizing a closed curve to start at some chosen point\<close>
+
+subsection \<open>Shift Path to Start at Some Given Point\<close>
 
 definition%important shiftpath :: "real \<Rightarrow> (real \<Rightarrow> 'a::topological_space) \<Rightarrow> real \<Rightarrow> 'a"
   where "shiftpath a f = (\<lambda>x. if (a + x) \<le> 1 then f (a + x) else f (a + x - 1))"
@@ -1164,7 +1168,8 @@
     by (force split: if_split_asm dest!: *)
 qed
 
-subsection \<open>Special case of straight-line paths\<close>
+
+subsection \<open>Straight-Line Paths\<close>
 
 definition%important linepath :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real \<Rightarrow> 'a"
   where "linepath a b = (\<lambda>x. (1 - x) *\<^sub>R a + x *\<^sub>R b)"
@@ -1385,6 +1390,7 @@
     by (force simp: inj_on_def)
 qed
 
+
 subsection%unimportant \<open>Bounding a point away from a path\<close>
 
 lemma not_on_path_ball:
@@ -1416,7 +1422,7 @@
 qed
 
 
-section \<open>Path component, considered as a "joinability" relation\<close>
+section \<open>Path component\<close>
 
 text \<open>(by Tom Hales)\<close>
 
@@ -1472,7 +1478,6 @@
   unfolding path_component_def
   by (rule_tac x="linepath a b" in exI, auto)
 
-
 subsubsection%unimportant \<open>Path components as sets\<close>
 
 lemma path_component_set:
@@ -1495,6 +1500,7 @@
    "y \<in> path_component_set s x \<Longrightarrow> path_component_set s y = path_component_set s x"
 by (metis (no_types, lifting) Collect_cong mem_Collect_eq path_component_sym path_component_trans)
 
+
 subsection \<open>Path connectedness of a space\<close>
 
 definition%important "path_connected s \<longleftrightarrow>
@@ -1804,6 +1810,7 @@
     using path_component_eq_empty by auto
 qed
 
+
 subsection%unimportant\<open>Lemmas about path-connectedness\<close>
 
 lemma path_connected_linear_image:
@@ -2523,7 +2530,7 @@
   by (meson cobounded_unique_unbounded_components connected_eq_connected_components_eq assms)
 
 
-section\<open>The "inside" and "outside" of a set\<close>
+section\<open>The \<open>inside\<close> and \<open>outside\<close> of a set\<close>
 
 text%important\<open>The inside comprises the points in a bounded connected component of the set's complement.
   The outside comprises the points in unbounded connected component of the complement.\<close>
@@ -3324,6 +3331,7 @@
   apply (metis cobounded_unique_unbounded_components connected_outside double_compl outside_bounded_nonempty outside_in_components unbounded_outside)
   by (simp add: connected_outside outside_bounded_nonempty outside_in_components unbounded_outside)
 
+
 subsection\<open>Condition for an open map's image to contain a ball\<close>
 
 proposition ball_subset_open_map_image:
@@ -3377,6 +3385,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>
 
 text%important\<open> We often just want to require that it fixes some subset, but to take in
@@ -3888,6 +3897,7 @@
   apply (auto simp: pathstart_def pathfinish_def elim!: homotopic_with_mono)
   done
 
+
 subsection\<open>Group properties for homotopy of paths\<close>
 
 text%important\<open>So taking equivalence classes under homotopy would give the fundamental group\<close>
@@ -4278,6 +4288,7 @@
     by (metis atLeastAtMost_iff imageI le_less_trans not_le path_image_def)
 qed
 
+
 subsection\<open> Homotopy and subpaths\<close>
 
 lemma homotopic_join_subpaths1:
@@ -4834,6 +4845,7 @@
     done
 qed
 
+
 subsection\<open>Local versions of topological properties in general\<close>
 
 definition%important locally :: "('a::topological_space set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
@@ -5065,6 +5077,7 @@
     done
 qed
 
+
 subsection\<open>An induction principle for connected sets\<close>
 
 proposition connected_induction:
@@ -5511,6 +5524,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>
 
 proposition Sura_Bura_compact:
@@ -6541,6 +6555,7 @@
   finally show ?thesis .
 qed
 
+
 subsection\<open>Retracts, in a general sense, preserve (co)homotopic triviality)\<close>
 
 locale%important Retracts =
@@ -6707,6 +6722,7 @@
     "S homeomorphic T \<Longrightarrow> (simply_connected S \<longleftrightarrow> simply_connected T)"
   by (metis homeomorphic_simply_connected homeomorphic_sym)
 
+
 subsection\<open>Homotopy equivalence\<close>
 
 definition%important homotopy_eqv :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
@@ -6997,6 +7013,7 @@
   shows "\<lbrakk>contractible S; S homeomorphic T\<rbrakk> \<Longrightarrow> contractible T"
   by (metis homeomorphic_contractible_eq)
 
+
 subsection%unimportant\<open>Misc other results\<close>
 
 lemma bounded_connected_Compl_real:
@@ -7041,6 +7058,7 @@
     by blast
 qed
 
+
 subsection%unimportant\<open>Some Uncountable Sets\<close>
 
 lemma uncountable_closed_segment:
@@ -7868,7 +7886,6 @@
     using homeomorphism_moving_points_exists_gen [OF \<open>finite K\<close> KS pw _ ope S] that by fastforce
 qed
 
-
 subsubsection%unimportant\<open>The theorem \<open>homeomorphism_grouping_points_exists\<close>\<close>
 
 lemma homeomorphism_grouping_point_1:
@@ -8337,6 +8354,7 @@
   qed
 qed
 
+
 subsection\<open>Nullhomotopic mappings\<close>
 
 text\<open> A mapping out of a sphere is nullhomotopic iff it extends to the ball.