src/HOL/Probability/Infinite_Product_Measure.thy
changeset 46898 1570b30ee040
parent 46731 5302e932d1e5
child 46905 6b1c0a80a57a
     1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 13 12:51:52 2012 +0100
     1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 13 13:31:26 2012 +0100
     1.3 @@ -502,7 +502,7 @@
     1.4      fix A assume "A \<in> sets ?G"
     1.5      with generatorE guess J X . note JX = this
     1.6      interpret JK: finite_product_prob_space M J by default fact+
     1.7 -    with JX show "\<mu>G A \<noteq> \<infinity>" by simp
     1.8 +    from JX show "\<mu>G A \<noteq> \<infinity>" by simp
     1.9    next
    1.10      fix A assume A: "range A \<subseteq> sets ?G" "decseq A" "(\<Inter>i. A i) = {}"
    1.11      then have "decseq (\<lambda>i. \<mu>G (A i))"