# HG changeset patch
# User hoelzl
# Date 1475243503 -7200
# Node ID 721810140424bfe6c251612650eca6a86d012c0b
# Parent  b09f16aeb694d149f06a22b824a07250c141eeeb
HOL-Analysis: fix latex generation

diff -r b09f16aeb694 -r 721810140424 src/HOL/Analysis/Path_Connected.thy
--- 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