diff -r be5461582d0f -r 739a9379e29b src/HOL/Probability/Borel.thy
--- a/src/HOL/Probability/Borel.thy	Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Probability/Borel.thy	Sun May 09 22:51:11 2010 -0700
@@ -68,9 +68,9 @@
     with w have "real(Suc(natceiling(inverse(g w - f w)))) > inverse(g w - f w)"
       by (metis lessI order_le_less_trans real_natceiling_ge real_of_nat_less_iff)       hence "inverse(real(Suc(natceiling(inverse(g w - f w)))))
              < inverse(inverse(g w - f w))" 
-      by (metis less_iff_diff_less_0 less_imp_inverse_less linorder_neqE_linordered_idom nz positive_imp_inverse_positive real_le_antisym real_less_def w)
+      by (metis less_iff_diff_less_0 less_imp_inverse_less linorder_neqE_linordered_idom nz positive_imp_inverse_positive order_antisym less_le w)
     hence "inverse(real(Suc(natceiling(inverse(g w - f w))))) < g w - f w"
-      by (metis inverse_inverse_eq order_less_le_trans real_le_refl) 
+      by (metis inverse_inverse_eq order_less_le_trans order_refl)
     thus "\<exists>n. f w \<le> g w - inverse(real(Suc n))" using w
       by (rule_tac x="natceiling(inverse(g w - f w))" in exI, auto)
   next
@@ -357,7 +357,7 @@
                     borel_measurable_uminus_borel_measurable f g)
   finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" .
   show ?thesis
-    apply (simp add: times_eq_sum_squares real_diff_def) 
+    apply (simp add: times_eq_sum_squares diff_def) 
     using 1 2 apply (simp add: borel_measurable_add_borel_measurable) 
     done
 qed
@@ -366,7 +366,7 @@
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
-unfolding real_diff_def
+unfolding diff_def
   by (fast intro: borel_measurable_add_borel_measurable 
                   borel_measurable_uminus_borel_measurable f g)
 
@@ -397,7 +397,7 @@
   { fix w
     from `0 < a` have "a \<le> inverse (f w) \<longleftrightarrow> 0 < f w \<and> f w \<le> 1 / a"
       by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le
-                linorder_not_le real_le_refl real_le_trans real_less_def
+                linorder_not_le order_refl order_trans less_le
                 xt1(7) zero_less_divide_1_iff) }
   hence "{w \<in> space M. a \<le> inverse (f w)} =
     {w \<in> space M. 0 < f w} \<inter> {w \<in> space M. f w \<le> 1 / a}" by auto
@@ -418,7 +418,7 @@
       apply (metis inverse_eq_divide linorder_not_le xt1(8) xt1(9)
                    zero_le_divide_1_iff)
       apply (metis inverse_eq_divide inverse_inverse_eq inverse_le_imp_le_neg
-                   linorder_not_le real_le_refl real_le_trans)
+                   linorder_not_le order_refl order_trans)
       done }
   hence "{w \<in> space M. a \<le> inverse (f w)} =
     {w \<in> space M. f w \<le> 1 / a} \<union> {w \<in> space M. 0 \<le> f w}" by auto
@@ -627,11 +627,11 @@
 proof -
   from assms have "y - z > 0" by simp
   hence A: "\<exists>n. (\<forall> m \<ge> n. \<bar> x m + - y \<bar> < y - z)" using assms
-    unfolding incseq_def LIMSEQ_def dist_real_def real_diff_def
+    unfolding incseq_def LIMSEQ_def dist_real_def diff_def
     by simp
   have "\<forall>m. x m \<le> y" using incseq_le assms by auto
   hence B: "\<forall>m. \<bar> x m + - y \<bar> = y - x m"
-    by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le real_diff_def)
+    by (metis abs_if abs_minus_add_cancel less_iff_diff_less_0 linorder_not_le diff_def)
   from A B show ?thesis by auto
 qed