# HG changeset patch
# User nipkow
# Date 1536132977 -7200
# Node ID 55b12fde48d02807182ee3f7cdb2f4e732558f10
# Parent  ecc76fa24a3202b54cf3323ac922830b96fb5d89
tuned

diff -r ecc76fa24a32 -r 55b12fde48d0 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Wed Sep 05 05:05:26 2018 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy	Wed Sep 05 09:36:17 2018 +0200
@@ -1412,7 +1412,9 @@
 qed
 
 
-section \<open>Path component, considered as a "joinability" relation (from Tom Hales)\<close>
+section \<open>Path component, considered as a "joinability" relation\<close>
+
+text \<open>(by Tom Hales)\<close>
 
 definition%important "path_component s x y \<longleftrightarrow>
   (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y)"