--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Nov 05 09:44:57 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Nov 05 09:44:58 2013 +0100
@@ -8724,7 +8724,7 @@
using interior_subset[of I] `x \<in> interior I` by auto
have "Inf (?F x) \<le> (f x - f y) / (x - y)"
- proof (rule cInf_lower2)
+ proof (intro bdd_belowI cInf_lower2)
show "(f x - f t) / (x - t) \<in> ?F x"
using `t \<in> I` `x < t` by auto
show "(f x - f t) / (x - t) \<le> (f x - f y) / (x - y)"