# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1475328103 -7200
# Node ID efc958d2fe007d29f1de67a6cfc82d565a5790e3
# Parent  ec0fb01c6d50d3699521ded75720946272f04a2a
repair LaTeX

diff -r ec0fb01c6d50 -r efc958d2fe00 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Sat Oct 01 12:03:27 2016 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy	Sat Oct 01 15:21:43 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>