diff -r 89d19aa73081 -r aa894a49f77d src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Sun Apr 17 22:38:50 2016 +0200
+++ b/src/HOL/Library/Convex.thy	Mon Apr 18 14:30:32 2016 +0100
@@ -65,13 +65,13 @@
 lemma convex_UNIV[intro,simp]: "convex UNIV"
   unfolding convex_def by auto
 
-lemma convex_Inter: "(\<forall>s\<in>f. convex s) \<Longrightarrow> convex(\<Inter>f)"
+lemma convex_Inter: "(\<And>s. s\<in>f \<Longrightarrow> convex s) \<Longrightarrow> convex(\<Inter>f)"
   unfolding convex_def by auto
 
 lemma convex_Int: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<inter> t)"
   unfolding convex_def by auto
 
-lemma convex_INT: "\<forall>i\<in>A. convex (B i) \<Longrightarrow> convex (\<Inter>i\<in>A. B i)"
+lemma convex_INT: "(\<And>i. i \<in> A \<Longrightarrow> convex (B i)) \<Longrightarrow> convex (\<Inter>i\<in>A. B i)"
   unfolding convex_def by auto
 
 lemma convex_Times: "convex s \<Longrightarrow> convex t \<Longrightarrow> convex (s \<times> t)"