# HG changeset patch
# User huffman
# Date 1273032230 25200
# Node ID 16b0a722083afa7490d798f588fab5ff63b0bd7c
# Parent  c90c8a3ae1f75986bffde53816974ce3f432dd74
avoid using '...' with LIMSEQ (cf. 1cc4ab4b7ff7)

diff -r c90c8a3ae1f7 -r 16b0a722083a src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Tue May 04 19:53:57 2010 -0700
+++ b/src/HOL/Probability/Measure.thy	Tue May 04 21:03:50 2010 -0700
@@ -463,7 +463,7 @@
   have "(measure M \<circ> nat_case {} A) ----> measure M (\<Union>i. nat_case {} A i)" 
     by (rule measure_countable_increasing) 
        (auto simp add: range_subsetD [OF A] subsetD [OF ASuc] split: nat.splits) 
-  also have "... = measure M (\<Union>i. A i)" 
+  also have "measure M (\<Union>i. nat_case {} A i) = measure M (\<Union>i. A i)" 
     by (simp add: ueq) 
   finally have "(measure M \<circ> nat_case {} A) ---->  measure M (\<Union>i. A i)" .
   thus ?thesis using meq
@@ -652,7 +652,7 @@
                   show "\<And>n. f -` A n \<inter> space m1 \<subseteq> f -` A (Suc n) \<inter> space m1"
                     using ASuc by auto
                 qed
-              also have "... = measure m1 (f -` (\<Union>i. A i) \<inter> space m1)"
+              also have "measure m1 (\<Union>i. f -` A i \<inter> space m1) = measure m1 (f -` (\<Union>i. A i) \<inter> space m1)"
                 by (simp add: vimage_UN)
               finally have "(measure m2 \<circ> A) ----> measure m1 (f -` (\<Union>i. A i) \<inter> space m1)" .
               moreover