src/HOL/Library/Convex_Euclidean_Space.thy

   thus ?thesis using assms unfolding shiftpath_def path_image_def pathfinish_def pathstart_def 
     by(auto simp add:vector_component_simps image_iff) qed
 
 subsection {* Special case of straight-line paths. *}
 
-definition "linepath a b = (\<lambda>x. (1 - dest_vec1 x) *s a + dest_vec1 x *s b)"
+definition
+  linepath :: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 1 \<Rightarrow> real ^ 'n" where
+  "linepath a b = (\<lambda>x. (1 - dest_vec1 x) *s a + dest_vec1 x *s b)"
 
 lemma pathstart_linepath[simp]: "pathstart(linepath a b) = a"
   unfolding pathstart_def linepath_def by auto
 
 lemma pathfinish_linepath[simp]: "pathfinish(linepath a b) = b"