src/HOL/Analysis/Path_Connected.thy
changeset 64911 f0e07600de47
parent 64790 ed38f9a834d8
child 65038 9391ea7daa17
     1.1 --- a/src/HOL/Analysis/Path_Connected.thy	Tue Jan 17 11:26:21 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Tue Jan 17 13:59:10 2017 +0100
     1.3 @@ -7099,7 +7099,7 @@
     1.4  
     1.5  subsection\<open> Self-homeomorphisms shuffling points about in various ways.\<close>
     1.6  
     1.7 -subsubsection\<open>The theorem @{text homeomorphism_moving_points_exists}\<close>
     1.8 +subsubsection\<open>The theorem \<open>homeomorphism_moving_points_exists\<close>\<close>
     1.9  
    1.10  lemma homeomorphism_moving_point_1:
    1.11    fixes a :: "'a::euclidean_space"
    1.12 @@ -7521,7 +7521,7 @@
    1.13  qed
    1.14  
    1.15  
    1.16 -subsubsection\<open>The theorem @{text homeomorphism_grouping_points_exists}\<close>
    1.17 +subsubsection\<open>The theorem \<open>homeomorphism_grouping_points_exists\<close>\<close>
    1.18  
    1.19  lemma homeomorphism_grouping_point_1:
    1.20    fixes a::real and c::real