# HG changeset patch
# User hoelzl
# Date 1450714132 -3600
# Node ID 8b4b5d74c5876a518fee0f29ee5a4413460d1095
# Parent  b4bfa62e799dcc7d26e5d2f4899f1a9e25a161d8
Probability: fix coercions (real ~> real_of_enat)

diff -r b4bfa62e799d -r 8b4b5d74c587 src/HOL/Probability/Interval_Integral.thy
--- a/src/HOL/Probability/Interval_Integral.thy	Mon Dec 21 14:44:44 2015 +0100
+++ b/src/HOL/Probability/Interval_Integral.thy	Mon Dec 21 17:08:52 2015 +0100
@@ -389,11 +389,11 @@
            simp add: interval_lebesgue_integral_def einterval_iff)
 
 lemma interval_integral_Ioi:
-  "\<bar>a\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..\<infinity>. f x) = (LBINT x : {real a <..}. f x)"
+  "\<bar>a\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..\<infinity>. f x) = (LBINT x : {real_of_ereal a <..}. f x)"
   by (auto simp add: interval_lebesgue_integral_def einterval_iff)
 
 lemma interval_integral_Ioo:
-  "a \<le> b \<Longrightarrow> \<bar>a\<bar> < \<infinity> ==> \<bar>b\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {real a <..< real b}. f x)"
+  "a \<le> b \<Longrightarrow> \<bar>a\<bar> < \<infinity> ==> \<bar>b\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {real_of_ereal a <..< real_of_ereal b}. f x)"
   by (auto simp add: interval_lebesgue_integral_def einterval_iff)
 
 lemma interval_integral_discrete_difference: