--- a/src/HOL/Analysis/Path_Connected.thy Tue Oct 25 11:55:38 2016 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Tue Oct 25 15:46:07 2016 +0100
@@ -1205,6 +1205,9 @@
lemma linepath_trivial [simp]: "linepath a a x = a"
by (simp add: linepath_def real_vector.scale_left_diff_distrib)
+lemma linepath_refl: "linepath a a = (\<lambda>x. a)"
+ by auto
+
lemma subpath_refl: "subpath a a g = linepath (g a) (g a)"
by (simp add: subpath_def linepath_def algebra_simps)
@@ -4362,6 +4365,7 @@
by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def)
qed
+
subsection\<open>Contractible sets\<close>
definition contractible where