--- a/src/HOL/Library/Convex_Euclidean_Space.thy Tue Jun 02 20:35:04 2009 -0700
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy Tue Jun 02 22:09:50 2009 -0700
@@ -1243,6 +1243,7 @@
lemma compact_convex_combinations:
+ fixes s t :: "(real ^ _) set"
assumes "compact s" "compact t"
shows "compact { (1 - u) *s x + u *s y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> t}"
proof-
@@ -1905,6 +1906,7 @@
subsection {* Homeomorphism of all convex compact sets with nonempty interior. *}
lemma compact_frontier_line_lemma:
+ fixes s :: "(real ^ _) set"
assumes "compact s" "0 \<in> s" "x \<noteq> 0"
obtains u where "0 \<le> u" "(u *s x) \<in> frontier s" "\<forall>v>u. (v *s x) \<notin> s"
proof-