src/HOL/Analysis/Lebesgue_Measure.thy

       "S \<subseteq> S'" and finS: "finite S" and
       Sprop: "{a'..b} \<subseteq> (\<Union>i \<in> S. {l i<..<r i + delta i})"
     proof (rule compactE_image)
       show "compact {a'..b}"
         by (rule compact_Icc)
-      show "\<forall>i \<in> S'. open ({l i<..<r i + delta i})" by auto
+      show "\<And>i. i \<in> S' \<Longrightarrow> open ({l i<..<r i + delta i})" by auto
       have "{a'..b} \<subseteq> {a <.. b}"
         by auto
       also have "{a <.. b} = (\<Union>i\<in>S'. {l i<..r i})"
         unfolding lr_eq_ab[symmetric] by (fastforce simp add: S'_def intro: less_le_trans)
       also have "\<dots> \<subseteq> (\<Union>i \<in> S'. {l i<..<r i + delta i})"