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/Probability/Infinite_Product_Measure.thy
changeset 51351 dd1dd470690b
parent 50252 4aa34bd43228
child 53015 a1119cf551e8 
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 05 15:43:21 2013 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 05 15:43:22 2013 +0100
@@ -303,7 +303,7 @@
       with `(\<Inter>i. A i) = {}` show False by auto
     qed
     ultimately show "(\<lambda>i. \<mu>G (A i)) ----> 0"
-      using LIMSEQ_ereal_INFI[of "\<lambda>i. \<mu>G (A i)"] by simp
+      using LIMSEQ_INF[of "\<lambda>i. \<mu>G (A i)"] by simp
   qed fact+
   then guess \<mu> .. note \<mu> = this
   show ?thesis
isabelle