--- a/src/HOL/Analysis/Path_Connected.thy Fri Sep 30 15:35:46 2016 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Fri Sep 30 15:51:43 2016 +0200
@@ -6582,7 +6582,7 @@
subsection\<open> Self-homeomorphisms shuffling points about in various ways.\<close>
-subsubsection\<open>The theorem @{text homeomorphism_moving_points_exists}}\<close>
+subsubsection\<open>The theorem @{text homeomorphism_moving_points_exists}\<close>
lemma homeomorphism_moving_point_1:
fixes a :: "'a::euclidean_space"
@@ -7004,7 +7004,7 @@
qed
-subsubsection\<open>The theorem @{text homeomorphism_grouping_points_exists}}\<close>
+subsubsection\<open>The theorem @{text homeomorphism_grouping_points_exists}\<close>
lemma homeomorphism_grouping_point_1:
fixes a::real and c::real