diff -r ffc5176a9105 -r eb2574ac4173 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Nov 16 12:09:59 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Nov 16 15:06:34 2009 +0100
@@ -379,6 +379,9 @@
   shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \<in> s"
   using assms unfolding convex_alt by auto
 
+lemma convex_vec1:"convex (vec1 ` s) = convex (s::real set)"
+  unfolding convex_def Ball_def forall_vec1 unfolding vec1_dest_vec1_simps image_iff by auto
+
 lemma convex_empty[intro]: "convex {}"
   unfolding convex_def by simp
 
@@ -3379,6 +3382,4 @@
 lemma connected_sphere: "2 \<le> CARD('n) \<Longrightarrow> connected {x::real^'n::finite. norm(x - a) = r}"
   using path_connected_sphere path_connected_imp_connected by auto
  
-(** In continuous_at_vec1_norm : Use \<And> instead of \<forall>. **)
-
 end