# HG changeset patch
# User immler
# Date 1572474628 14400
# Node ID 196b41b9b9c88ef8f08d305c42887429e360891b
# Parent  82057e7b9ea0ae26bbbfa99f3f4ee5b61964dd4c# Parent  80dfc9a2f9c81e3f4d676a12e89ebd8d40bdcdd4
merged

diff -r 80dfc9a2f9c8 -r 196b41b9b9c8 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Wed Oct 30 21:14:57 2019 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Wed Oct 30 18:30:28 2019 -0400
@@ -815,7 +815,7 @@
 lemma subpath_translation: "subpath u v ((\<lambda>x. a + x) \<circ> g) = (\<lambda>x. a + x) \<circ> subpath u v g"
   by (rule ext) (simp add: subpath_def)
 
-lemma subpath_linear_image: "linear f \<Longrightarrow> subpath u v (f \<circ> g) = f \<circ> subpath u v g"
+lemma subpath_image: "subpath u v (f \<circ> g) = f \<circ> subpath u v g"
   by (rule ext) (simp add: subpath_def)
 
 lemma affine_ineq: