--- 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>