src/HOL/Probability/Finite_Product_Measure.thy
changeset 49999 dfb63b9b8908
parent 49784 5e5b2da42a69
child 50003 8c213922ed49
     1.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 02 12:00:51 2012 +0100
     1.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Fri Nov 02 14:00:39 2012 +0100
     1.3 @@ -795,7 +795,7 @@
     1.4    show ?thesis
     1.5      apply (subst distr_merge[OF IJ, symmetric])
     1.6      apply (subst positive_integral_distr[OF measurable_merge f])
     1.7 -    apply (subst P.positive_integral_fst_measurable(2)[symmetric, OF P_borel])
     1.8 +    apply (subst J.positive_integral_fst_measurable(2)[symmetric, OF P_borel])
     1.9      apply simp
    1.10      done
    1.11  qed