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