--- a/src/HOL/Multivariate_Analysis/Integration.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Sun Mar 16 18:09:04 2014 +0100
@@ -18,7 +18,7 @@
lemma cInf_abs_ge: (* TODO: is this really needed? *)
fixes S :: "real set"
shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
- by (simp add: Inf_real_def) (rule cSup_abs_le, auto)
+ by (simp add: Inf_real_def) (insert cSup_abs_le [of "uminus ` S"], auto)
lemma cSup_asclose: (* TODO: is this really needed? *)
fixes S :: "real set"