--- a/src/HOL/Analysis/Path_Connected.thy Sat Oct 01 19:30:21 2016 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Sat Oct 01 20:03:17 2016 +0200
@@ -7482,7 +7482,7 @@
subsection\<open>nullhomotopic mappings\<close>
text\<open> A mapping out of a sphere is nullhomotopic iff it extends to the ball.
-This even works out in the degenerate cases when the radius is \<le> 0, and
+This even works out in the degenerate cases when the radius is \<open>\<le>\<close> 0, and
we also don't need to explicitly assume continuity since it's already implicit
in both sides of the equivalence.\<close>