changeset 44568 e6f291cb5810 parent 43923 ab93d0190a5d child 44890 22f665a2e91c
```     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Sat Aug 27 17:26:14 2011 +0200
1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Sun Aug 28 09:20:12 2011 -0700
1.3 @@ -209,7 +209,7 @@
1.4      from finite_continuity_from_below[OF _ A] `range A \<subseteq> sets M`
1.5        M'.finite_continuity_from_below[OF _ A]
1.6      have convergent: "(\<lambda>i. ?d (A i)) ----> ?d (\<Union>i. A i)"
1.7 -      by (auto intro!: LIMSEQ_diff)
1.8 +      by (auto intro!: tendsto_diff)
1.9      obtain n :: nat where "- ?d (\<Union>i. A i) / e < real n" using reals_Archimedean2 by auto
1.10      moreover from order_trans[OF decseq_le[OF decseq convergent] dA_less]
1.11      have "real n \<le> - ?d (\<Union>i. A i) / e" using `0<e` by (simp add: field_simps)
1.12 @@ -295,7 +295,7 @@
1.13      from
1.14        finite_continuity_from_above[OF `range A \<subseteq> sets M` A]
1.15        M'.finite_continuity_from_above[OF `range A \<subseteq> sets M` A]
1.16 -    have "(\<lambda>i. ?d (A i)) ----> ?d (\<Inter>i. A i)" by (intro LIMSEQ_diff)
1.17 +    have "(\<lambda>i. ?d (A i)) ----> ?d (\<Inter>i. A i)" by (intro tendsto_diff)
1.18      thus "?d (space M) \<le> ?d (\<Inter>i. A i)" using mono_dA[THEN monoD, of 0 _]
1.19        by (rule_tac LIMSEQ_le_const) (auto intro!: exI)
1.20    next
```