# HG changeset patch # User Lars Hupel # 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\nullhomotopic mappings\ text\ 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 \ 0, and +This even works out in the degenerate cases when the radius is \\\ 0, and we also don't need to explicitly assume continuity since it's already implicit in both sides of the equivalence.\