--- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Wed Apr 02 18:35:02 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Wed Apr 02 18:35:07 2014 +0200
@@ -110,7 +110,7 @@
proof atomize_elim
let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
from assms have "compact ?proj" "?proj \<noteq> {}"
- by (auto intro!: compact_continuous_image continuous_on_intros)
+ by (auto intro!: compact_continuous_image continuous_intros)
from compact_attains_inf[OF this]
obtain s x
where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> s \<le> t"
@@ -133,7 +133,7 @@
proof atomize_elim
let ?proj = "(\<lambda>x. x \<bullet> b) ` X"
from assms have "compact ?proj" "?proj \<noteq> {}"
- by (auto intro!: compact_continuous_image continuous_on_intros)
+ by (auto intro!: compact_continuous_image continuous_intros)
from compact_attains_sup[OF this]
obtain s x
where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> t \<le> s"