# HG changeset patch
# User hoelzl
# Date 1358420237 -3600
# Node ID cfdf19d3ca326501b32761bbe17468d6c334113f
# Parent  a076e01b803f7cc84d9468a030c877e9ae44f127
generalize compact_path_image to topological_space

diff -r a076e01b803f -r cfdf19d3ca32 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Thu Jan 17 14:15:10 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Thu Jan 17 11:57:17 2013 +0100
@@ -57,7 +57,7 @@
   apply (rule convex_connected, rule convex_real_interval)
   done
 
-lemma compact_path_image[intro]: "path g \<Longrightarrow> compact(path_image g :: 'a::metric_space set)"
+lemma compact_path_image[intro]: "path g \<Longrightarrow> compact(path_image g)"
   unfolding path_def path_image_def
   by (erule compact_continuous_image, rule compact_interval)