--- a/src/HOL/Analysis/Path_Connected.thy Mon Oct 28 20:51:38 2019 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Wed Oct 30 15:26:10 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: