Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Analysis/Lebesgue_Measure.thy
changeset 65585 a043de9ad41e
parent 65204 d23eded35a33
child 65680 378a2f11bec9 
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Wed Apr 26 15:57:16 2017 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Wed Apr 26 16:58:31 2017 +0100
@@ -220,7 +220,7 @@
     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})"
isabelle