# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1483977288 0
# Node ID 54f5afc9c41389d3339a5491790249c33ee165ac
# Parent  de4e3df6693dc4dfd7bd334ed25485c020b7523d
fixed LaTeX problems

diff -r de4e3df6693d -r 54f5afc9c413 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Mon Jan 09 14:40:31 2017 +0000
+++ b/src/HOL/Analysis/Further_Topology.thy	Mon Jan 09 15:54:48 2017 +0000
@@ -3037,7 +3037,7 @@
   shows "0 < r \<Longrightarrow> \<not> simply_connected(sphere a r)"
 by (simp add: simply_connected_sphere_eq)
 
-  
+
 proposition simply_connected_punctured_convex:
   fixes a :: "'a::euclidean_space"
   assumes "convex S" and 3: "3 \<le> aff_dim S"
@@ -4100,8 +4100,8 @@
 
 subsection\<open>The "Borsukian" property of sets\<close>
 
-text\<open>This doesn't have a standard name. Kuratowski uses "contractible with respect to [S^1]"
- while Whyburn uses "property b". It's closely related to unicoherence.\<close>
+text\<open>This doesn't have a standard name. Kuratowski uses ``contractible with respect to $[S^1]$''
+ while Whyburn uses ``property b''. It's closely related to unicoherence.\<close>
 
 definition Borsukian where
     "Borsukian S \<equiv>