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/Measure_Space.thy
changeset 70532 fcf3b891ccb1
parent 70380 2b0dca68c3ee
child 70614 6a2c982363e9 
--- a/src/HOL/Analysis/Measure_Space.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -2335,7 +2335,7 @@
       then have eq: "(\<Union>i. F i) = F i"
         by auto
       with i show ?thesis
-        by (auto intro!: Lim_transform_eventually[OF _ tendsto_const] eventually_sequentiallyI[where c=i])
+        by (auto intro!: Lim_transform_eventually[OF tendsto_const] eventually_sequentiallyI[where c=i])
     next
       assume "\<not> (\<exists>i. \<forall>j\<ge>i. F i = F j)"
       then obtain f where f: "\<And>i. i \<le> f i" "\<And>i. F i \<noteq> F (f i)" by metis
isabelle