summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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