src/HOL/Probability/Probability_Space.thy
changeset 41661 baf1964bc468
parent 41545 9c869baf1c66
child 41689 3e39b0e730d6
     1.1 --- a/src/HOL/Probability/Probability_Space.thy	Fri Jan 21 11:39:26 2011 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Space.thy	Mon Jan 24 22:29:50 2011 +0100
     1.3 @@ -195,8 +195,8 @@
     1.4    assumes "random_variable S X"
     1.5    shows "prob_space S (distribution X)"
     1.6  proof -
     1.7 -  interpret S: measure_space S "distribution X"
     1.8 -    using measure_space_vimage[of X S] assms unfolding distribution_def by simp
     1.9 +  interpret S: measure_space S "distribution X" unfolding distribution_def
    1.10 +    using assms by (intro measure_space_vimage) auto
    1.11    show ?thesis
    1.12    proof
    1.13      have "X -` space S \<inter> space M = space M"