--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Mar 17 21:56:32 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Tue Mar 18 10:12:57 2014 +0100
@@ -44,7 +44,7 @@
by auto
lemma path_image_nonempty: "path_image g \<noteq> {}"
- unfolding path_image_def image_is_empty interval_eq_empty
+ unfolding path_image_def image_is_empty box_eq_empty
by auto
lemma pathstart_in_path_image[intro]: "pathstart g \<in> path_image g"
@@ -64,7 +64,7 @@
lemma compact_path_image[intro]: "path g \<Longrightarrow> compact (path_image g)"
unfolding path_def path_image_def
apply (erule compact_continuous_image)
- apply (rule compact_interval)
+ apply (rule compact_Icc)
done
lemma reversepath_reversepath[simp]: "reversepath (reversepath g) = g"