--- a/src/HOL/Library/Convex_Euclidean_Space.thy Fri May 29 15:32:33 2009 -0700
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy Fri May 29 18:23:07 2009 -0700
@@ -615,7 +615,7 @@
subsection {* One rather trivial consequence. *}
-lemma connected_UNIV: "connected UNIV"
+lemma connected_UNIV: "connected (UNIV :: (real ^ _) set)"
by(simp add: convex_connected convex_UNIV)
subsection {* Convex functions into the reals. *}
@@ -763,10 +763,10 @@
thus "dist x (u *s y + v *s z) \<le> e" using real_convex_bound_le[OF yz uv] by auto
qed
-lemma connected_ball: "connected(ball x e)"
+lemma connected_ball: "connected(ball (x::real^_) e)" (* FIXME: generalize *)
using convex_connected convex_ball by auto
-lemma connected_cball: "connected(cball x e)"
+lemma connected_cball: "connected(cball (x::real^_) e)" (* FIXME: generalize *)
using convex_connected convex_cball by auto
subsection {* Convex hull. *}
@@ -2186,7 +2186,9 @@
ultimately show "u *s x + v *s y \<in> s" apply- apply(rule assms[unfolded is_interval_def, rule_format, OF as(1,2)])
using as(3-) dimindex_ge_1 apply- by(auto simp add: vector_component) qed
-lemma is_interval_connected: "is_interval s \<Longrightarrow> connected s"
+lemma is_interval_connected:
+ fixes s :: "(real ^ _) set"
+ shows "is_interval s \<Longrightarrow> connected s"
using is_interval_convex convex_connected by auto
lemma convex_interval: "convex {a .. b}" "convex {a<..<b::real^'n::finite}"