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/Projective_Limit.thy
changeset 51351 dd1dd470690b
parent 50971 5e3d3d690975
child 52681 8cc7f76b827a 
--- a/src/HOL/Probability/Projective_Limit.thy	Tue Mar 05 15:43:21 2013 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy	Tue Mar 05 15:43:22 2013 +0100
@@ -515,7 +515,7 @@
       thus False using Z by simp
     qed
     ultimately show "(\<lambda>i. \<mu>G (Z i)) ----> 0"
-      using LIMSEQ_ereal_INFI[of "\<lambda>i. \<mu>G (Z i)"] by simp
+      using LIMSEQ_INF[of "\<lambda>i. \<mu>G (Z i)"] by simp
   qed
   then guess \<mu> .. note \<mu> = this
   def f \<equiv> "finmap_of J B"
isabelle