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