real is better supported than real_of_nat, use it in the nat => ereal coercion

--- a/src/HOL/Library/Extended_Real.thy	Mon Dec 05 14:47:01 2011 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Mon Dec 05 17:33:57 2011 +0100
@@ -59,7 +59,7 @@
 
 declare [[coercion "ereal :: real \<Rightarrow> ereal"]]
 declare [[coercion "ereal_of_enat :: enat \<Rightarrow> ereal"]]
-declare [[coercion "(\<lambda>n. ereal (of_nat n)) :: nat \<Rightarrow> ereal"]]
+declare [[coercion "(\<lambda>n. ereal (real n)) :: nat \<Rightarrow> ereal"]]
 
 lemma ereal_uminus_uminus[simp]:
   fixes a :: ereal shows "- (- a) = a"

--- a/src/HOL/Probability/Radon_Nikodym.thy	Mon Dec 05 14:47:01 2011 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Mon Dec 05 17:33:57 2011 +0100
@@ -1097,7 +1097,7 @@
       next
         case (real r)
         with less_PInf_Ex_of_nat[of "f x"] obtain n :: nat where "f x < n" by (auto simp: real_eq_of_nat)
-        then show ?thesis using x real unfolding A_def by (auto intro!: exI[of _ "Suc n"])
+        then show ?thesis using x real unfolding A_def by (auto intro!: exI[of _ "Suc n"] simp: real_eq_of_nat)
       next
         case MInf with x show ?thesis
           unfolding A_def by (auto intro!: exI[of _ "Suc 0"])
@@ -1117,7 +1117,7 @@
       case (Suc n)
       then have "(\<integral>\<^isup>+x. f x * indicator (A i \<inter> Q j) x \<partial>M) \<le>
         (\<integral>\<^isup>+x. (Suc n :: ereal) * indicator (Q j) x \<partial>M)"
-        by (auto intro!: positive_integral_mono simp: indicator_def A_def)
+        by (auto intro!: positive_integral_mono simp: indicator_def A_def real_eq_of_nat)
       also have "\<dots> = Suc n * \<mu> (Q j)"
         using Q by (auto intro!: positive_integral_cmult_indicator)
       also have "\<dots> < \<infinity>"