src/HOL/Probability/Probability_Measure.thy
changeset 43340 60e181c4eae4
parent 43339 9ba256ad6781
child 43556 0d78c8d31d0d
     1.1 --- a/src/HOL/Probability/Probability_Measure.thy	Thu Jun 09 13:55:11 2011 +0200
     1.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Thu Jun 09 14:04:34 2011 +0200
     1.3 @@ -275,7 +275,7 @@
     1.4  proof -
     1.5    have "expectation X < expectation (\<lambda>x. b)"
     1.6      using gt measure_space_1
     1.7 -    by (intro integral_less_AE) auto
     1.8 +    by (intro integral_less_AE_space) auto
     1.9    then show ?thesis using prob_space by simp
    1.10  qed
    1.11  
    1.12 @@ -286,7 +286,7 @@
    1.13  proof -
    1.14    have "expectation (\<lambda>x. a) < expectation X"
    1.15      using gt measure_space_1
    1.16 -    by (intro integral_less_AE) auto
    1.17 +    by (intro integral_less_AE_space) auto
    1.18    then show ?thesis using prob_space by simp
    1.19  qed
    1.20