summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Probability/Probability_Measure.thy

changeset 43340 | 60e181c4eae4 |

parent 43339 | 9ba256ad6781 |

child 43556 | 0d78c8d31d0d |

--- a/src/HOL/Probability/Probability_Measure.thy Thu Jun 09 13:55:11 2011 +0200 +++ b/src/HOL/Probability/Probability_Measure.thy Thu Jun 09 14:04:34 2011 +0200 @@ -275,7 +275,7 @@ proof - have "expectation X < expectation (\<lambda>x. b)" using gt measure_space_1 - by (intro integral_less_AE) auto + by (intro integral_less_AE_space) auto then show ?thesis using prob_space by simp qed @@ -286,7 +286,7 @@ proof - have "expectation (\<lambda>x. a) < expectation X" using gt measure_space_1 - by (intro integral_less_AE) auto + by (intro integral_less_AE_space) auto then show ?thesis using prob_space by simp qed