# HG changeset patch
# User huffman
# Date 1273470671 25200
# Node ID 739a9379e29b06bfa24d1026a2455dde13f1c0f2
# Parent  be5461582d0f92acb7bfac4d94268dff0b8369d3
avoid using real-specific versions of generic lemmas

diff -r be5461582d0f -r 739a9379e29b src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sun May 09 22:51:11 2010 -0700
@@ -18,7 +18,7 @@
   shows "a 0 - x * (\<Sum> i=0..<n. (-1)^i * a (Suc i) * x^i) = (\<Sum> i=0..<Suc n. (-1)^i * a i * x^i)"
 proof -
   have shift_pow: "\<And>i. - (x * ((-1)^i * a (Suc i) * x ^ i)) = (-1)^(Suc i) * a (Suc i) * x ^ (Suc i)" by auto
-  show ?thesis unfolding setsum_right_distrib shift_pow real_diff_def setsum_negf[symmetric] setsum_head_upt_Suc[OF zero_less_Suc]
+  show ?thesis unfolding setsum_right_distrib shift_pow diff_def setsum_negf[symmetric] setsum_head_upt_Suc[OF zero_less_Suc]
     setsum_reindex[OF inj_Suc, unfolded comp_def, symmetric, of "\<lambda> n. (-1)^n  *a n * x^n"] by auto
 qed
 
@@ -109,8 +109,8 @@
   proof (rule setsum_cong, simp)
     fix j assume "j \<in> {0 ..< n}"
     show "1 / real (f (j' + j)) * real x ^ j = -1 ^ j * (1 / real (f (j' + j))) * real (- x) ^ j"
-      unfolding move_minus power_mult_distrib real_mult_assoc[symmetric]
-      unfolding real_mult_commute unfolding real_mult_assoc[of "-1 ^ j", symmetric] power_mult_distrib[symmetric]
+      unfolding move_minus power_mult_distrib mult_assoc[symmetric]
+      unfolding mult_commute unfolding mult_assoc[of "-1 ^ j", symmetric] power_mult_distrib[symmetric]
       by auto
   qed
 
@@ -435,8 +435,8 @@
 
   { have "real (x * lb_arctan_horner prec n 1 (x*x)) \<le> ?S n"
       using bounds(1) `0 \<le> real x`
-      unfolding real_of_float_mult power_add power_one_right real_mult_assoc[symmetric] setsum_left_distrib[symmetric]
-      unfolding real_mult_commute mult_commute[of _ "2::nat"] power_mult power2_eq_square[of "real x"]
+      unfolding real_of_float_mult power_add power_one_right mult_assoc[symmetric] setsum_left_distrib[symmetric]
+      unfolding mult_commute[where 'a=real] mult_commute[of _ "2::nat"] power_mult power2_eq_square[of "real x"]
       by (auto intro!: mult_left_mono)
     also have "\<dots> \<le> arctan (real x)" using arctan_bounds ..
     finally have "real (x * lb_arctan_horner prec n 1 (x*x)) \<le> arctan (real x)" . }
@@ -444,8 +444,8 @@
   { have "arctan (real x) \<le> ?S (Suc n)" using arctan_bounds ..
     also have "\<dots> \<le> real (x * ub_arctan_horner prec (Suc n) 1 (x*x))"
       using bounds(2)[of "Suc n"] `0 \<le> real x`
-      unfolding real_of_float_mult power_add power_one_right real_mult_assoc[symmetric] setsum_left_distrib[symmetric]
-      unfolding real_mult_commute mult_commute[of _ "2::nat"] power_mult power2_eq_square[of "real x"]
+      unfolding real_of_float_mult power_add power_one_right mult_assoc[symmetric] setsum_left_distrib[symmetric]
+      unfolding mult_commute[where 'a=real] mult_commute[of _ "2::nat"] power_mult power2_eq_square[of "real x"]
       by (auto intro!: mult_left_mono)
     finally have "arctan (real x) \<le> real (x * ub_arctan_horner prec (Suc n) 1 (x*x))" . }
   ultimately show ?thesis by auto
@@ -616,7 +616,7 @@
         using arctan_0_1_bounds[OF `0 \<le> real ?DIV` `real ?DIV \<le> 1`] by auto
       also have "\<dots> \<le> 2 * arctan (real x / ?R)"
         using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
-      also have "2 * arctan (real x / ?R) = arctan (real x)" using arctan_half[symmetric] unfolding numeral_2_eq_2 power_Suc2 power_0 real_mult_1 .
+      also have "2 * arctan (real x / ?R) = arctan (real x)" using arctan_half[symmetric] unfolding numeral_2_eq_2 power_Suc2 power_0 mult_1_left .
       finally show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF True] .
     next
       case False
@@ -644,7 +644,7 @@
           using `0 \<le> arctan (real x)` arctan_inverse[OF `1 / real x \<noteq> 0`]
           unfolding real_sgn_pos[OF `0 < 1 / real x`] le_diff_eq by auto
         moreover
-        have "real (lb_pi prec * Float 1 -1) \<le> pi / 2" unfolding real_of_float_mult Float_num times_divide_eq_right real_mult_1 using pi_boundaries by auto
+        have "real (lb_pi prec * Float 1 -1) \<le> pi / 2" unfolding real_of_float_mult Float_num times_divide_eq_right mult_1_left using pi_boundaries by auto
         ultimately
         show ?thesis unfolding lb_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_not_P[OF `\<not> x \<le> Float 1 1`] if_not_P[OF False]
           by auto
@@ -696,7 +696,7 @@
       show ?thesis
       proof (cases "?DIV > 1")
         case True
-        have "pi / 2 \<le> real (ub_pi prec * Float 1 -1)" unfolding real_of_float_mult Float_num times_divide_eq_right real_mult_1 using pi_boundaries by auto
+        have "pi / 2 \<le> real (ub_pi prec * Float 1 -1)" unfolding real_of_float_mult Float_num times_divide_eq_right mult_1_left using pi_boundaries by auto
         from order_less_le_trans[OF arctan_ubound this, THEN less_imp_le]
         show ?thesis unfolding ub_arctan.simps Let_def if_not_P[OF `\<not> x < 0`] if_not_P[OF `\<not> x \<le> Float 1 -1`] if_P[OF `x \<le> Float 1 1`] if_P[OF True] .
       next
@@ -706,7 +706,7 @@
         have "0 \<le> real x / ?R" using `0 \<le> real x` `0 < ?R` unfolding real_0_le_divide_iff by auto
         hence "0 \<le> real ?DIV" using monotone by (rule order_trans)
 
-        have "arctan (real x) = 2 * arctan (real x / ?R)" using arctan_half unfolding numeral_2_eq_2 power_Suc2 power_0 real_mult_1 .
+        have "arctan (real x) = 2 * arctan (real x / ?R)" using arctan_half unfolding numeral_2_eq_2 power_Suc2 power_0 mult_1_left .
         also have "\<dots> \<le> 2 * arctan (real ?DIV)"
           using arctan_monotone'[OF monotone] by (auto intro!: mult_left_mono)
         also have "\<dots> \<le> real (Float 1 1 * ?ub_horner ?DIV)" unfolding real_of_float_mult[of "Float 1 1"] Float_num
@@ -912,8 +912,8 @@
   from horner_bounds[where lb="lb_sin_cos_aux prec" and ub="ub_sin_cos_aux prec" and j'=0,
     OF `0 \<le> real (x * x)` f_eq lb_sin_cos_aux.simps ub_sin_cos_aux.simps]
   show "?lb" and "?ub" using `0 \<le> real x` unfolding real_of_float_mult
-    unfolding power_add power_one_right real_mult_assoc[symmetric] setsum_left_distrib[symmetric]
-    unfolding real_mult_commute
+    unfolding power_add power_one_right mult_assoc[symmetric] setsum_left_distrib[symmetric]
+    unfolding mult_commute[where 'a=real]
     by (auto intro!: mult_left_mono simp add: power_mult power2_eq_square[of "real x"])
 qed
 
@@ -1179,7 +1179,7 @@
 proof (induct n arbitrary: x)
   case (Suc n)
   have split_pi_off: "x + real (Suc n) * 2 * pi = (x + real n * 2 * pi) + 2 * pi"
-    unfolding Suc_eq_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
+    unfolding Suc_eq_plus1 real_of_nat_add real_of_one left_distrib by auto
   show ?case unfolding split_pi_off using Suc by auto
 qed auto
 
@@ -1213,7 +1213,7 @@
           round_down[of prec "lb_pi prec"] by auto
   hence "real ?lx \<le> x - real k * 2 * pi \<and> x - real k * 2 * pi \<le> real ?ux"
     using x by (cases "k = 0") (auto intro!: add_mono
-                simp add: real_diff_def k[symmetric] less_float_def)
+                simp add: diff_def k[symmetric] less_float_def)
   note lx = this[THEN conjunct1] and ux = this[THEN conjunct2]
   hence lx_less_ux: "real ?lx \<le> real ?ux" by (rule order_trans)
 
@@ -1227,7 +1227,7 @@
     also have "\<dots> \<le> cos (x + real (-k) * 2 * pi)"
       using cos_monotone_minus_pi_0'[OF pi_lx lx x_le_0]
       by (simp only: real_of_float_minus real_of_int_minus
-        cos_minus real_diff_def mult_minus_left)
+        cos_minus diff_def mult_minus_left)
     finally have "real (lb_cos prec (- ?lx)) \<le> cos x"
       unfolding cos_periodic_int . }
   note negative_lx = this
@@ -1240,7 +1240,7 @@
     have "cos (x + real (-k) * 2 * pi) \<le> cos (real ?lx)"
       using cos_monotone_0_pi'[OF lx_0 lx pi_x]
       by (simp only: real_of_float_minus real_of_int_minus
-        cos_minus real_diff_def mult_minus_left)
+        cos_minus diff_def mult_minus_left)
     also have "\<dots> \<le> real (ub_cos prec ?lx)"
       using lb_cos[OF lx_0 pi_lx] by simp
     finally have "cos x \<le> real (ub_cos prec ?lx)"
@@ -1255,7 +1255,7 @@
     have "cos (x + real (-k) * 2 * pi) \<le> cos (real (- ?ux))"
       using cos_monotone_minus_pi_0'[OF pi_x ux ux_0]
       by (simp only: real_of_float_minus real_of_int_minus
-          cos_minus real_diff_def mult_minus_left)
+          cos_minus diff_def mult_minus_left)
     also have "\<dots> \<le> real (ub_cos prec (- ?ux))"
       using lb_cos_minus[OF pi_ux ux_0, of prec] by simp
     finally have "cos x \<le> real (ub_cos prec (- ?ux))"
@@ -1272,7 +1272,7 @@
     also have "\<dots> \<le> cos (x + real (-k) * 2 * pi)"
       using cos_monotone_0_pi'[OF x_ge_0 ux pi_ux]
       by (simp only: real_of_float_minus real_of_int_minus
-        cos_minus real_diff_def mult_minus_left)
+        cos_minus diff_def mult_minus_left)
     finally have "real (lb_cos prec ?ux) \<le> cos x"
       unfolding cos_periodic_int . }
   note positive_ux = this
@@ -1347,7 +1347,7 @@
       also have "\<dots> \<le> cos (real (?ux - 2 * ?lpi))"
         using cos_monotone_minus_pi_0'[OF pi_x x_le_ux ux_0]
         by (simp only: real_of_float_minus real_of_int_minus real_of_one
-            number_of_Min real_diff_def mult_minus_left real_mult_1)
+            number_of_Min diff_def mult_minus_left mult_1_left)
       also have "\<dots> = cos (real (- (?ux - 2 * ?lpi)))"
         unfolding real_of_float_minus cos_minus ..
       also have "\<dots> \<le> real (ub_cos prec (- (?ux - 2 * ?lpi)))"
@@ -1391,7 +1391,7 @@
       also have "\<dots> \<le> cos (real (?lx + 2 * ?lpi))"
         using cos_monotone_0_pi'[OF lx_0 lx_le_x pi_x]
         by (simp only: real_of_float_minus real_of_int_minus real_of_one
-          number_of_Min real_diff_def mult_minus_left real_mult_1)
+          number_of_Min diff_def mult_minus_left mult_1_left)
       also have "\<dots> \<le> real (ub_cos prec (?lx + 2 * ?lpi))"
         using lb_cos[OF lx_0 pi_lx] by simp
       finally show ?thesis unfolding u by (simp add: real_of_float_max)
@@ -1531,7 +1531,7 @@
     hence "real (floor_fl x) < 0" unfolding Float_floor real_of_float_simp using zero_less_pow2[of xe] by auto
     hence "m < 0"
       unfolding less_float_def real_of_float_0 Float_floor real_of_float_simp
-      unfolding pos_prod_lt[OF zero_less_pow2[of e], unfolded real_mult_commute] by auto
+      unfolding pos_prod_lt[OF zero_less_pow2[of e], unfolded mult_commute] by auto
     hence "1 \<le> - m" by auto
     hence "0 < nat (- m)" by auto
     moreover
@@ -1682,7 +1682,7 @@
   { fix n have "?a (Suc n) \<le> ?a n" unfolding inverse_eq_divide[symmetric]
     proof (rule mult_mono)
       show "0 \<le> x ^ Suc (Suc n)" by (auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`)
-      have "x ^ Suc (Suc n) \<le> x ^ Suc n * 1" unfolding power_Suc2 real_mult_assoc[symmetric]
+      have "x ^ Suc (Suc n) \<le> x ^ Suc n * 1" unfolding power_Suc2 mult_assoc[symmetric]
         by (rule mult_left_mono, fact less_imp_le[OF `x < 1`], auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`)
       thus "x ^ Suc (Suc n) \<le> x ^ Suc n" by auto
     qed auto }
@@ -1700,7 +1700,7 @@
 
   let "?s n" = "-1^n * (1 / real (1 + n)) * (real x)^(Suc n)"
 
-  have "?lb \<le> setsum ?s {0 ..< 2 * ev}" unfolding power_Suc2 real_mult_assoc[symmetric] real_of_float_mult setsum_left_distrib[symmetric] unfolding real_mult_commute[of "real x"] ev
+  have "?lb \<le> setsum ?s {0 ..< 2 * ev}" unfolding power_Suc2 mult_assoc[symmetric] real_of_float_mult setsum_left_distrib[symmetric] unfolding mult_commute[of "real x"] ev
     using horner_bounds(1)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x" and lb="\<lambda>n i k x. lb_ln_horner prec n k x" and ub="\<lambda>n i k x. ub_ln_horner prec n k x" and j'=1 and n="2*ev",
       OF `0 \<le> real x` refl lb_ln_horner.simps ub_ln_horner.simps] `0 \<le> real x`
     by (rule mult_right_mono)
@@ -1708,7 +1708,7 @@
   finally show "?lb \<le> ?ln" .
 
   have "?ln \<le> setsum ?s {0 ..< 2 * od + 1}" using ln_bounds(2)[OF `0 \<le> real x` `real x < 1`] by auto
-  also have "\<dots> \<le> ?ub" unfolding power_Suc2 real_mult_assoc[symmetric] real_of_float_mult setsum_left_distrib[symmetric] unfolding real_mult_commute[of "real x"] od
+  also have "\<dots> \<le> ?ub" unfolding power_Suc2 mult_assoc[symmetric] real_of_float_mult setsum_left_distrib[symmetric] unfolding mult_commute[of "real x"] od
     using horner_bounds(2)[where G="\<lambda> i k. Suc k" and F="\<lambda>x. x" and f="\<lambda>x. x" and lb="\<lambda>n i k x. lb_ln_horner prec n k x" and ub="\<lambda>n i k x. ub_ln_horner prec n k x" and j'=1 and n="2*od+1",
       OF `0 \<le> real x` refl lb_ln_horner.simps ub_ln_horner.simps] `0 \<le> real x`
     by (rule mult_right_mono)
@@ -2088,28 +2088,28 @@
 "interpret_floatarith (Var n) vs     = vs ! n"
 
 lemma interpret_floatarith_divide: "interpret_floatarith (Mult a (Inverse b)) vs = (interpret_floatarith a vs) / (interpret_floatarith b vs)"
-  unfolding real_divide_def interpret_floatarith.simps ..
+  unfolding divide_inverse interpret_floatarith.simps ..
 
 lemma interpret_floatarith_diff: "interpret_floatarith (Add a (Minus b)) vs = (interpret_floatarith a vs) - (interpret_floatarith b vs)"
-  unfolding real_diff_def interpret_floatarith.simps ..
+  unfolding diff_def interpret_floatarith.simps ..
 
 lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) vs =
   sin (interpret_floatarith a vs)"
   unfolding sin_cos_eq interpret_floatarith.simps
-            interpret_floatarith_divide interpret_floatarith_diff real_diff_def
+            interpret_floatarith_divide interpret_floatarith_diff diff_def
   by auto
 
 lemma interpret_floatarith_tan:
   "interpret_floatarith (Mult (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) (Inverse (Cos a))) vs =
    tan (interpret_floatarith a vs)"
-  unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def real_divide_def
+  unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def divide_inverse
   by auto
 
 lemma interpret_floatarith_powr: "interpret_floatarith (Exp (Mult b (Ln a))) vs = (interpret_floatarith a vs) powr (interpret_floatarith b vs)"
   unfolding powr_def interpret_floatarith.simps ..
 
 lemma interpret_floatarith_log: "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs = log (interpret_floatarith b vs) (interpret_floatarith x vs)"
-  unfolding log_def interpret_floatarith.simps real_divide_def ..
+  unfolding log_def interpret_floatarith.simps divide_inverse ..
 
 lemma interpret_floatarith_num:
   shows "interpret_floatarith (Num (Float 0 0)) vs = 0"
diff -r be5461582d0f -r 739a9379e29b src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Decision_Procs/MIR.thy	Sun May 09 22:51:11 2010 -0700
@@ -2177,7 +2177,7 @@
     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
     hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
-      by (simp only:  real_mult_less_mono2[OF rcpos th1])
+      by (simp only: mult_strict_left_mono [OF th1 rcpos])
     hence "real c * real x + Inum (y # bs) e \<noteq> 0"using rcpos  by simp
     thus "real c * real x + Inum (real x # bs) e \<noteq> 0" 
       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"]  by simp
@@ -2194,7 +2194,7 @@
     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
     hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
-      by (simp only:  real_mult_less_mono2[OF rcpos th1])
+      by (simp only: mult_strict_left_mono [OF th1 rcpos])
     hence "real c * real x + Inum (y # bs) e \<noteq> 0"using rcpos  by simp
     thus "real c * real x + Inum (real x # bs) e \<noteq> 0" 
       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"]  by simp
@@ -2211,7 +2211,7 @@
     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
     hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
-      by (simp only:  real_mult_less_mono2[OF rcpos th1])
+      by (simp only: mult_strict_left_mono [OF th1 rcpos])
     thus "real c * real x + Inum (real x # bs) e < 0" 
       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
   qed
@@ -2227,7 +2227,7 @@
     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
     hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
-      by (simp only:  real_mult_less_mono2[OF rcpos th1])
+      by (simp only: mult_strict_left_mono [OF th1 rcpos])
     thus "real c * real x + Inum (real x # bs) e \<le> 0" 
       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
   qed
@@ -2243,7 +2243,7 @@
     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
     hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
-      by (simp only:  real_mult_less_mono2[OF rcpos th1])
+      by (simp only: mult_strict_left_mono [OF th1 rcpos])
     thus "\<not> (real c * real x + Inum (real x # bs) e>0)" 
       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
   qed
@@ -2259,7 +2259,7 @@
     assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
     hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
-      by (simp only:  real_mult_less_mono2[OF rcpos th1])
+      by (simp only: mult_strict_left_mono [OF th1 rcpos])
     thus "\<not> real c * real x + Inum (real x # bs) e \<ge> 0" 
       using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
   qed
diff -r be5461582d0f -r 739a9379e29b src/HOL/Hahn_Banach/Function_Norm.thy
--- a/src/HOL/Hahn_Banach/Function_Norm.thy	Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Sun May 09 22:51:11 2010 -0700
@@ -124,7 +124,7 @@
           assume "y \<noteq> 0"
           with y obtain x where y_rep: "y = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
               and x: "x \<in> V" and neq: "x \<noteq> 0"
-            by (auto simp add: B_def real_divide_def)
+            by (auto simp add: B_def divide_inverse)
           from x neq have gt: "0 < \<parallel>x\<parallel>" ..
 
           txt {* The thesis follows by a short calculation using the
@@ -139,7 +139,7 @@
             then show "0 \<le> inverse \<parallel>x\<parallel>" by (rule order_less_imp_le)
           qed
           also have "\<dots> = c * (\<parallel>x\<parallel> * inverse \<parallel>x\<parallel>)"
-            by (rule real_mult_assoc)
+            by (rule Groups.mult_assoc)
           also
           from gt have "\<parallel>x\<parallel> \<noteq> 0" by simp
           then have "\<parallel>x\<parallel> * inverse \<parallel>x\<parallel> = 1" by simp 
@@ -224,7 +224,7 @@
     proof (rule mult_right_mono)
       from x show "0 \<le> \<parallel>x\<parallel>" ..
       from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
-        by (auto simp add: B_def real_divide_def)
+        by (auto simp add: B_def divide_inverse)
       with `continuous V norm f` show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
         by (rule fn_norm_ub)
     qed
@@ -257,7 +257,7 @@
       assume "b \<noteq> 0"
       with b obtain x where b_rep: "b = \<bar>f x\<bar> * inverse \<parallel>x\<parallel>"
         and x_neq: "x \<noteq> 0" and x: "x \<in> V"
-        by (auto simp add: B_def real_divide_def)
+        by (auto simp add: B_def divide_inverse)
       note b_rep
       also have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> (c * \<parallel>x\<parallel>) * inverse \<parallel>x\<parallel>"
       proof (rule mult_right_mono)
diff -r be5461582d0f -r 739a9379e29b src/HOL/Hahn_Banach/Vector_Space.thy
--- a/src/HOL/Hahn_Banach/Vector_Space.thy	Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Sun May 09 22:51:11 2010 -0700
@@ -118,7 +118,7 @@
 proof -
   assume x: "x \<in> V"
   have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
-    by (simp add: real_diff_def)
+    by (simp add: diff_def)
   also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x"
     by (rule add_mult_distrib2)
   also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)"
@@ -255,7 +255,7 @@
 
 lemma (in vectorspace) mult_left_commute:
     "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = b \<cdot> a \<cdot> x"
-  by (simp add: real_mult_commute mult_assoc2)
+  by (simp add: mult_commute mult_assoc2)
 
 lemma (in vectorspace) mult_zero_uniq:
   "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> a \<cdot> x = 0 \<Longrightarrow> a = 0"
diff -r be5461582d0f -r 739a9379e29b src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Library/Convex.thy	Sun May 09 22:51:11 2010 -0700
@@ -362,8 +362,7 @@
   { assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
     hence "\<mu> > 0" "(1 - \<mu>) > 0" using asms by auto
     hence "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms
-      using add_nonneg_pos[of "\<mu> *\<^sub>R x" "(1 - \<mu>) *\<^sub>R y"]
-        real_mult_order by auto fastsimp }
+      by (auto simp add: add_pos_pos mult_pos_pos) }
   ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0" using assms by fastsimp
 qed
 
@@ -426,7 +425,7 @@
     also have "\<dots> = f ((1 - a i) *\<^sub>R (\<Sum> j \<in> s. (a j * inverse (1 - a i)) *\<^sub>R y j) + a i *\<^sub>R y i)"
       using scaleR_right.setsum[of "inverse (1 - a i)" "\<lambda> j. a j *\<^sub>R y j" s, symmetric] by (auto simp:algebra_simps)
     also have "\<dots> = f ((1 - a i) *\<^sub>R (\<Sum> j \<in> s. ?a j *\<^sub>R y j) + a i *\<^sub>R y i)"
-      by (auto simp:real_divide_def)
+      by (auto simp: divide_inverse)
     also have "\<dots> \<le> (1 - a i) *\<^sub>R f ((\<Sum> j \<in> s. ?a j *\<^sub>R y j)) + a i * f (y i)"
       using conv[of "y i" "(\<Sum> j \<in> s. ?a j *\<^sub>R y j)" "a i", OF yai(1) asum yai(2) ai1]
       by (auto simp add:add_commute)
@@ -555,7 +554,7 @@
     from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0" by auto
     from mult_right_mono_neg[OF this le(2)]
     have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \<le> 0 * (x - y)"
-      unfolding diff_def using real_add_mult_distrib by auto
+      by (simp add: algebra_simps)
     hence "f' y * (x - y) - (f x - f y) \<le> 0" using le by auto
     hence res: "f' y * (x - y) \<le> f x - f y" by auto
     have "(f y - f x) / (y - x) - f' x = f' z1 - f' x"
@@ -570,7 +569,7 @@
     from cool this have "(f y - f x) / (y - x) - f' x \<ge> 0" by auto
     from mult_right_mono[OF this ge(2)]
     have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \<ge> 0 * (y - x)"
-      unfolding diff_def using real_add_mult_distrib by auto
+      by (simp add: algebra_simps)
     hence "f y - f x - f' x * (y - x) \<ge> 0" using ge by auto
     hence "f y - f x \<ge> f' x * (y - x)" "f' y * (x - y) \<le> f x - f y"
       using res by auto } note less_imp = this
@@ -606,9 +605,9 @@
   have "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))"
     by auto
   hence f''0: "\<And> z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
-    unfolding inverse_eq_divide by (auto simp add:real_mult_assoc)
+    unfolding inverse_eq_divide by (auto simp add: mult_assoc)
   have f''_ge0: "\<And> z :: real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
-    using `b > 1` by (auto intro!:less_imp_le simp add:divide_pos_pos[of 1] real_mult_order)
+    using `b > 1` by (auto intro!:less_imp_le simp add:divide_pos_pos[of 1] mult_pos_pos)
   from f''_ge0_imp_convex[OF pos_is_convex,
     unfolded greaterThan_iff, OF f' f''0 f''_ge0]
   show ?thesis by auto
diff -r be5461582d0f -r 739a9379e29b src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Library/Float.thy	Sun May 09 22:51:11 2010 -0700
@@ -508,7 +508,7 @@
   have "real m < 2^(nat (-e))" using `Float m e < 1`
     unfolding less_float_def real_of_float_neg_exp[OF `e < 0`] real_of_float_1
           real_mult_less_iff1[of _ _ 1, OF `0 < 2^(nat (-e))`, symmetric] 
-          real_mult_assoc by auto
+          mult_assoc by auto
   thus ?thesis unfolding real_of_int_less_iff[symmetric] by auto
 qed
 
@@ -619,7 +619,7 @@
   case True show ?thesis unfolding real_of_float_simp pow2_def using True by auto
 next
   case False hence P: "\<not> 0 \<le> - (bitlen m - 1)" using bitlen_ge1[OF `m \<noteq> 0`] by auto
-  show ?thesis unfolding real_of_float_nge0_exp[OF P] real_divide_def by auto
+  show ?thesis unfolding real_of_float_nge0_exp[OF P] divide_inverse by auto
 qed
 
 lemma bitlen_Pls: "bitlen (Int.Pls) = Int.Pls" by (subst Pls_def, subst Pls_def, simp)
@@ -683,7 +683,7 @@
   have "real (x * 2^?l div y) * inverse (2^?l) \<le> (real (x * 2^?l) / real y) * inverse (2^?l)" 
     by (rule mult_right_mono, fact real_of_int_div4, simp)
   also have "\<dots> \<le> (real x / real y) * 2^?l * inverse (2^?l)" by auto
-  finally have "real (x * 2^?l div y) * inverse (2^?l) \<le> real x / real y" unfolding real_mult_assoc by auto
+  finally have "real (x * 2^?l div y) * inverse (2^?l) \<le> real x / real y" unfolding mult_assoc by auto
   thus ?thesis unfolding lapprox_posrat_def Let_def normfloat real_of_float_simp
     unfolding pow2_minus pow2_int minus_minus .
 qed
@@ -700,7 +700,7 @@
     unfolding real_of_int_mult[symmetric] real_of_int_le_iff zmult_commute by auto
   hence "real (x div y) * real c * inverse (real c) \<le> real (x * c div y) * inverse (real c)"
     using `0 < c` by auto
-  thus ?thesis unfolding real_mult_assoc using `0 < c` by auto
+  thus ?thesis unfolding mult_assoc using `0 < c` by auto
 qed
 
 lemma lapprox_posrat_bottom: assumes "0 < y"
@@ -757,7 +757,7 @@
       by (rule divide_right_mono, simp only: `0 \<le> real y * 2^?l`)
     also have "\<dots> = real y * real (?X div y + 1) / real y / 2^?l" by auto
     also have "\<dots> = real (?X div y + 1) * inverse (2^?l)" unfolding nonzero_mult_divide_cancel_left[OF `real y \<noteq> 0`] 
-      unfolding real_divide_def ..
+      unfolding divide_inverse ..
     finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
       unfolding pow2_minus pow2_int minus_minus by auto
   qed
@@ -856,7 +856,7 @@
       finally have "real y * 2^nat (bitlen x - 1) * inverse (2^nat (bitlen x - 1)) \<le> real x * 2^nat (int (n - 1) + bitlen y) * inverse (2^nat (bitlen x - 1))"
         unfolding real_of_int_le_iff[symmetric] by auto
       hence "real y \<le> real x * (2^nat (int (n - 1) + bitlen y) / (2^nat (bitlen x - 1)))" 
-        unfolding real_mult_assoc real_divide_def by auto
+        unfolding mult_assoc divide_inverse by auto
       also have "\<dots> = real x * (2^(nat (int (n - 1) + bitlen y) - nat (bitlen x - 1)))" using power_diff[of "2::real", OF _ len_less] by auto
       finally have "y \<le> x * 2^?l" unfolding exp_eq unfolding real_of_int_le_iff[symmetric] by auto
       thus ?thesis using zdiv_greater_zero[OF `0 < y`] by auto
@@ -1083,7 +1083,7 @@
     hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m" unfolding div_mult_self2_is_id[OF `m \<noteq> 0`] .
     hence "2^(prec - 1) * inverse (2 ^ nat (int prec + bitlen m - 1)) \<le> ?d"
       unfolding real_of_int_le_iff[of "2^(prec - 1)", symmetric] by auto }
-  from mult_left_mono[OF this[unfolded pow_split power_add inverse_mult_distrib real_mult_assoc[symmetric] right_inverse[OF pow_not0] real_mult_1], of "2^?e"]
+  from mult_left_mono[OF this[unfolded pow_split power_add inverse_mult_distrib mult_assoc[symmetric] right_inverse[OF pow_not0] mult_1_left], of "2^?e"]
   have "2^?e * inverse (2^?b) \<le> 2^?e * ?d" unfolding pow_split power_add by auto
   finally have "1 \<le> 2^?e * ?d" .
   
@@ -1269,7 +1269,7 @@
       also have "\<dots> = real m" unfolding zmod_zdiv_equality[symmetric] ..
       finally show ?thesis by auto
     qed
-    thus ?thesis unfolding lb_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add real_mult_commute real_mult_assoc by auto
+    thus ?thesis unfolding lb_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add mult_commute mult_assoc by auto
   qed
   also have "\<dots> = real (x * y)" unfolding normfloat ..
   finally show ?thesis .
@@ -1293,10 +1293,10 @@
       
       have "real m = real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding zmod_zdiv_equality[symmetric] ..
       also have "\<dots> = real (m div 2^(nat ?l)) * 2^(nat ?l) + real (m mod 2^(nat ?l))" unfolding real_of_int_add by auto
-      also have "\<dots> \<le> (real (m div 2^(nat ?l)) + 1) * 2^(nat ?l)" unfolding real_add_mult_distrib using mod_uneq by auto
+      also have "\<dots> \<le> (real (m div 2^(nat ?l)) + 1) * 2^(nat ?l)" unfolding left_distrib using mod_uneq by auto
       finally show ?thesis unfolding pow2_int[symmetric] using True by auto
     qed
-    thus ?thesis unfolding ub_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add real_mult_commute real_mult_assoc by auto
+    thus ?thesis unfolding ub_mult_def Float Let_def float.cases if_P[OF True] real_of_float_simp pow2_add mult_commute mult_assoc by auto
   qed
   finally show ?thesis .
 qed
@@ -1329,7 +1329,7 @@
     hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
     have "real (Float (m div (2 ^ (nat (-e)))) 0) = real (m div 2 ^ (nat (-e)))" unfolding real_of_float_simp by auto
     also have "\<dots> \<le> real m / real ((2::int) ^ (nat (-e)))" using real_of_int_div4 .
-    also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_int_power real_number_of real_divide_def ..
+    also have "\<dots> = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_int_power real_number_of divide_inverse ..
     also have "\<dots> = real (Float m e)" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
     finally show ?thesis unfolding Float floor_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .
   next
@@ -1357,7 +1357,7 @@
     case False
     hence me_eq: "pow2 (-e) = pow2 (int (nat (-e)))" by auto
     have "real (Float m e) = real m * inverse (2 ^ (nat (-e)))" unfolding real_of_float_simp me_eq pow2_int pow2_neg[of e] ..
-    also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding real_of_int_power real_number_of real_divide_def ..
+    also have "\<dots> = real m / real ((2::int) ^ (nat (-e)))" unfolding real_of_int_power real_number_of divide_inverse ..
     also have "\<dots> \<le> 1 + real (m div 2 ^ (nat (-e)))" using real_of_int_div3[unfolded diff_le_eq] .
     also have "\<dots> = real (Float (m div (2 ^ (nat (-e))) + 1) 0)" unfolding real_of_float_simp by auto
     finally show ?thesis unfolding Float ceiling_fl.simps if_not_P[OF `\<not> 0 \<le> e`] .
diff -r be5461582d0f -r 739a9379e29b src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sun May 09 22:51:11 2010 -0700
@@ -355,7 +355,7 @@
     from real_lbound_gt_zero[OF one0 em0]
     obtain d where d: "d >0" "d < 1" "d < e / m" by blast
     from d(1,3) m(1) have dm: "d*m > 0" "d*m < e"
-      by (simp_all add: field_simps real_mult_order)
+      by (simp_all add: field_simps mult_pos_pos)
     show ?case
       proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
         fix d w
diff -r be5461582d0f -r 739a9379e29b src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sun May 09 22:51:11 2010 -0700
@@ -1589,7 +1589,7 @@
       thus ?thesis unfolding setsum_delta[OF assms(1)] using uv(2) and `u v < 0` and uv(1) by auto qed
   qed (insert setsum_nonneg_eq_0_iff[of _ u, OF fin(1)] uv(2-3), auto)
 
-  hence *:"setsum u {x\<in>c. u x > 0} > 0" unfolding real_less_def apply(rule_tac conjI, rule_tac setsum_nonneg) by auto
+  hence *:"setsum u {x\<in>c. u x > 0} > 0" unfolding less_le apply(rule_tac conjI, rule_tac setsum_nonneg) by auto
   moreover have "setsum u ({x \<in> c. 0 < u x} \<union> {x \<in> c. u x < 0}) = setsum u c"
     "(\<Sum>x\<in>{x \<in> c. 0 < u x} \<union> {x \<in> c. u x < 0}. u x *\<^sub>R x) = (\<Sum>x\<in>c. u x *\<^sub>R x)"
     using assms(1) apply(rule_tac[!] setsum_mono_zero_left) by auto
@@ -1943,7 +1943,7 @@
   apply (drule_tac x="\<lambda>i. (x i, f (x i))" in spec)
   apply simp
   using assms[unfolded convex] apply simp
-  apply(rule_tac j="\<Sum>i = 1..k. u i * f (fst (x i))" in real_le_trans)
+  apply(rule_tac y="\<Sum>i = 1..k. u i * f (fst (x i))" in order_trans)
   defer apply(rule setsum_mono) apply(erule_tac x=i in allE) unfolding real_scaleR_def
   apply(rule mult_left_mono)using assms[unfolded convex] by auto
 
@@ -2182,7 +2182,7 @@
         have "f x \<le> 1 / (1 + t) * f w + (t / (1 + t)) * f y" 
           using assms(2)[unfolded convex_on_def,rule_format,of w y "1/(1+t)" "t / (1+t)",unfolded w]
           using `0<t` `2<t` and `y\<in>s` `w\<in>s` by (auto simp add:field_simps)
-        also have "\<dots> = (f w + t * f y) / (1 + t)" using `t>0` unfolding real_divide_def by (auto simp add:field_simps)
+        also have "\<dots> = (f w + t * f y) / (1 + t)" using `t>0` unfolding divide_inverse by (auto simp add:field_simps)
         also have "\<dots> < e + f y" using `t>0` * `e>0` by(auto simp add:field_simps)
         finally have "f x - f y < e" by auto }
       ultimately show ?thesis by auto 
@@ -2231,7 +2231,7 @@
     apply(rule subset_trans[OF _ e(1)]) unfolding subset_eq mem_cball proof 
     fix z assume z:"z\<in>{x - ?d..x + ?d}"
     have e:"e = setsum (\<lambda>i. d) (UNIV::'n set)" unfolding setsum_constant d_def using dimge1
-      by (metis eq_divide_imp times_divide_eq_left real_dimindex_gt_0 real_eq_of_nat real_less_def real_mult_commute)
+      by (metis eq_divide_imp times_divide_eq_left real_dimindex_gt_0 real_eq_of_nat less_le mult_commute)
     show "dist x z \<le> e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
       using z[unfolded mem_interval] apply(erule_tac x=i in allE) by auto qed
   hence k:"\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption
@@ -2411,7 +2411,7 @@
       by(auto simp add: Cart_eq field_simps) 
     also have "\<dots> = abs(1/e) * norm (x - e *\<^sub>R (x - c) - y)" by(auto intro!:norm_eqI simp add: algebra_simps)
     also have "\<dots> < d" using as[unfolded dist_norm] and `e>0`
-      by(auto simp add:pos_divide_less_eq[OF `e>0`] real_mult_commute)
+      by(auto simp add:pos_divide_less_eq[OF `e>0`] mult_commute)
     finally show "y \<in> s" apply(subst *) apply(rule assms(1)[unfolded convex_alt,rule_format])
       apply(rule d[unfolded subset_eq,rule_format]) unfolding mem_ball using assms(3-5) by auto
   qed(rule mult_pos_pos, insert `e>0` `d>0`, auto) qed
@@ -2522,7 +2522,7 @@
   show ?thesis apply(rule that[of ?a]) unfolding interior_std_simplex mem_Collect_eq proof(rule,rule)
     fix i::'n show "0 < ?a $ i" unfolding ** using dimindex_ge_1 by(auto simp add: Suc_le_eq) next
     have "setsum (op $ ?a) ?D = setsum (\<lambda>i. inverse (2 * real CARD('n))) ?D" by(rule setsum_cong2, rule **) 
-    also have "\<dots> < 1" unfolding setsum_constant card_enum real_eq_of_nat real_divide_def[THEN sym] by (auto simp add:field_simps)
+    also have "\<dots> < 1" unfolding setsum_constant card_enum real_eq_of_nat divide_inverse[THEN sym] by (auto simp add:field_simps)
     finally show "setsum (op $ ?a) ?D < 1" by auto qed qed
 
 end
diff -r be5461582d0f -r 739a9379e29b src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun May 09 22:51:11 2010 -0700
@@ -3677,7 +3677,7 @@
   from Sup_finite_in[OF fS S0] 
   show ?thesis unfolding infnorm_def infnorm_set_image 
     by (metis Sup_finite_ge_iff finite finite_imageI UNIV_not_empty image_is_empty 
-              rangeI real_le_refl)
+              rangeI order_refl)
 qed
 
 lemma infnorm_mul_lemma: "infnorm(a *s x) <= \<bar>a\<bar> * infnorm x"
diff -r be5461582d0f -r 739a9379e29b src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sun May 09 22:51:11 2010 -0700
@@ -2195,7 +2195,7 @@
   shows "norm(setsum (\<lambda>l. content l *\<^sub>R c) p) \<le> e * content({a..b})" (is "?l \<le> ?r")
   apply(rule order_trans,rule setsum_norm) defer unfolding norm_scaleR setsum_left_distrib[THEN sym]
   apply(rule order_trans[OF mult_left_mono],rule assms,rule setsum_abs_ge_zero)
-  apply(subst real_mult_commute) apply(rule mult_left_mono)
+  apply(subst mult_commute) apply(rule mult_left_mono)
   apply(rule order_trans[of _ "setsum content p"]) apply(rule eq_refl,rule setsum_cong2)
   apply(subst abs_of_nonneg) unfolding additive_content_division[OF assms(1)]
 proof- from order_trans[OF norm_ge_zero[of c] assms(2)] show "0 \<le> e" .
@@ -2210,7 +2210,7 @@
 next case False show ?thesis
     apply(rule order_trans,rule setsum_norm) defer unfolding split_def norm_scaleR
     apply(rule order_trans[OF setsum_mono]) apply(rule mult_left_mono[OF _ abs_ge_zero, of _ e]) defer
-    unfolding setsum_left_distrib[THEN sym] apply(subst real_mult_commute) apply(rule mult_left_mono)
+    unfolding setsum_left_distrib[THEN sym] apply(subst mult_commute) apply(rule mult_left_mono)
     apply(rule order_trans[of _ "setsum (content \<circ> snd) p"]) apply(rule eq_refl,rule setsum_cong2)
     apply(subst o_def, rule abs_of_nonneg)
   proof- show "setsum (content \<circ> snd) p \<le> content {a..b}" apply(rule eq_refl)
@@ -2395,7 +2395,7 @@
             using g(1)[OF x, of n] g(1)[OF x, of m] by auto
         also have "\<dots> \<le> inverse (real M) + inverse (real M)" apply(rule add_mono)
           apply(rule_tac[!] le_imp_inverse_le) using goal1 M by auto
-        also have "\<dots> = 2 / real M" unfolding real_divide_def by auto
+        also have "\<dots> = 2 / real M" unfolding divide_inverse by auto
         finally show "norm (g n x - g m x) \<le> 2 / real M"
           using norm_triangle_le[of "g n x - f x" "f x - g m x" "2 / real M"]
           by(auto simp add:algebra_simps simp add:norm_minus_commute)
@@ -2672,7 +2672,7 @@
       also have "... \<le> setsum (\<lambda>i. e / 2 / 2 ^ i) {0..N+1}" apply(rule setsum_mono) 
       proof- case goal1 thus ?case apply(subst mult_commute, subst pos_le_divide_eq[THEN sym])
           using d(2)[rule_format,of "q i" i] using q[rule_format] by(auto simp add:field_simps)
-      qed also have "... < e * inverse 2 * 2" unfolding real_divide_def setsum_right_distrib[THEN sym]
+      qed also have "... < e * inverse 2 * 2" unfolding divide_inverse setsum_right_distrib[THEN sym]
         apply(rule mult_strict_left_mono) unfolding power_inverse atLeastLessThanSuc_atLeastAtMost[THEN sym]
         apply(subst sumr_geometric) using goal1 by auto
       finally show "?goal" by auto qed qed qed
@@ -3261,7 +3261,7 @@
             using as by(auto simp add:field_simps)
         next assume as:"0 > m i" hence *:"max (m i * a $ i) (m i * b $ i) = m i * a $ i"
             "min (m i * a $ i) (m i * b $ i) = m i * b $ i" using ab as unfolding min_def max_def 
-            by(auto simp add:field_simps mult_le_cancel_left_neg intro:real_le_antisym)
+            by(auto simp add:field_simps mult_le_cancel_left_neg intro: order_antisym)
           show ?thesis unfolding * apply rule defer apply(rule_tac x="1 / m i * x$i" in exI)
             using as by(auto simp add:field_simps) qed qed qed qed qed 
 
@@ -3567,7 +3567,7 @@
       hence "c$1 - t$1 < e / 3 / norm (f c)" by auto
       hence "norm (c - t) < e / 3 / norm (f c)" using as unfolding norm_vector_1 vector_less_def by auto
       thus "norm (f c) * norm (c - t) < e / 3" using False apply-
-        apply(subst real_mult_commute) apply(subst pos_less_divide_eq[THEN sym]) by auto
+        apply(subst mult_commute) apply(subst pos_less_divide_eq[THEN sym]) by auto
     qed next case True show ?thesis apply(rule_tac x=1 in exI) unfolding True using `e>0` by auto
   qed then guess w .. note w = conjunctD2[OF this,rule_format]
   
@@ -4408,8 +4408,8 @@
   next  case goal1 have *:"k * real (card r) / (1 + real (card r)) < k" using k by(auto simp add:field_simps)
     show ?case apply(rule le_less_trans[of _ "setsum (\<lambda>x. k / (real (card r) + 1)) r"])
       unfolding setsum_subtractf[THEN sym] apply(rule setsum_norm_le,fact)
-      apply rule apply(drule qq) defer unfolding real_divide_def setsum_left_distrib[THEN sym]
-      unfolding real_divide_def[THEN sym] using * by(auto simp add:field_simps real_eq_of_nat)
+      apply rule apply(drule qq) defer unfolding divide_inverse setsum_left_distrib[THEN sym]
+      unfolding divide_inverse[THEN sym] using * by(auto simp add:field_simps real_eq_of_nat)
   qed finally show "?x \<le> e + k" . qed
 
 lemma henstock_lemma_part2: fixes f::"real^'m \<Rightarrow> real^'n"
@@ -4525,7 +4525,7 @@
              apply(rule le_less_trans[of _ "setsum (\<lambda>i. e / 2^(i+2)) {0..s}"])
              apply(rule setsum_norm_le[OF finite_atLeastAtMost])
            proof show "(\<Sum>i = 0..s. e / 2 ^ (i + 2)) < e / 2"
-               unfolding power_add real_divide_def inverse_mult_distrib
+               unfolding power_add divide_inverse inverse_mult_distrib
                unfolding setsum_right_distrib[THEN sym] setsum_left_distrib[THEN sym]
                unfolding power_inverse sum_gp apply(rule mult_strict_left_mono[OF _ e])
                unfolding power2_eq_square by auto
diff -r be5461582d0f -r 739a9379e29b src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun May 09 22:51:11 2010 -0700
@@ -1777,7 +1777,7 @@
           by (auto simp add: norm_minus_commute)
         also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
           unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
-          unfolding real_add_mult_distrib using `x\<noteq>y`[unfolded dist_nz, unfolded dist_norm] by auto
+          unfolding left_distrib using `x\<noteq>y`[unfolded dist_nz, unfolded dist_norm] by auto
         also have "\<dots> \<le> e - d/2" using `d \<le> dist x y` and `d>0` and `?rhs` by(auto simp add: dist_norm)
         finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using `d>0` by auto
 
@@ -2104,10 +2104,10 @@
   { fix x assume "x\<in>S"
     hence "norm x \<le> b" using b by auto
     hence "norm (f x) \<le> B * b" using B(2) apply(erule_tac x=x in allE)
-      by (metis B(1) B(2) real_le_trans real_mult_le_cancel_iff2)
+      by (metis B(1) B(2) order_trans mult_le_cancel_left_pos)
   }
   thus ?thesis unfolding bounded_pos apply(rule_tac x="b*B" in exI)
-    using b B real_mult_order[of b B] by (auto simp add: real_mult_commute)
+    using b B mult_pos_pos [of b B] by (auto simp add: mult_commute)
 qed
 
 lemma bounded_scaling:
@@ -3061,7 +3061,7 @@
     { fix e::real assume "e>0"
       hence "dist a b < e" using assms(4 )using b using a by blast
     }
-    hence "dist a b = 0" by (metis dist_eq_0_iff dist_nz real_less_def)
+    hence "dist a b = 0" by (metis dist_eq_0_iff dist_nz less_le)
   }
   with a have "\<Inter>(range s) = {a}" unfolding image_def by auto
   thus ?thesis ..
@@ -3841,7 +3841,7 @@
 proof-
   { fix x assume "x \<in> s"
     then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> s" using assms(2)[unfolded open_dist, THEN bspec[where x=x]] by auto
-    have "e * abs c > 0" using assms(1)[unfolded zero_less_abs_iff[THEN sym]] using real_mult_order[OF `e>0`] by auto
+    have "e * abs c > 0" using assms(1)[unfolded zero_less_abs_iff[THEN sym]] using mult_pos_pos[OF `e>0`] by auto
     moreover
     { fix y assume "dist y (c *\<^sub>R x) < e * \<bar>c\<bar>"
       hence "norm ((1 / c) *\<^sub>R y - x) < e" unfolding dist_norm
@@ -5015,7 +5015,7 @@
 lemma is_interval_interval: "is_interval {a .. b::real^'n}" (is ?th1) "is_interval {a<..<b}" (is ?th2) proof - 
   have *:"\<And>x y z::real. x < y \<Longrightarrow> y < z \<Longrightarrow> x < z" by auto
   show ?th1 ?th2  unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
-    by(meson real_le_trans le_less_trans less_le_trans *)+ qed
+    by(meson order_trans le_less_trans less_le_trans *)+ qed
 
 lemma is_interval_empty:
  "is_interval {}"
@@ -5423,7 +5423,7 @@
       hence "(norm a / norm x) *\<^sub>R x \<in> {x \<in> s. norm x = norm a}" using `x\<in>s` and `x\<noteq>0` by auto
       thus "norm (f b) / norm b * norm x \<le> norm (f x)" using b[THEN bspec[where x="(norm a / norm x) *\<^sub>R x"]]
         unfolding f.scaleR and ba using `x\<noteq>0` `a\<noteq>0`
-        by (auto simp add: real_mult_commute pos_le_divide_eq pos_divide_le_eq)
+        by (auto simp add: mult_commute pos_le_divide_eq pos_divide_le_eq)
     qed }
   ultimately
   show ?thesis by auto
@@ -5647,14 +5647,14 @@
       unfolding image_iff Bex_def mem_interval vector_le_def
       apply(auto simp add: vector_smult_assoc pth_3[symmetric]
         intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
-      by(auto simp add: pos_le_divide_eq pos_divide_le_eq real_mult_commute diff_le_iff)
+      by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff)
   } moreover
   { fix y assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
     hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
       unfolding image_iff Bex_def mem_interval vector_le_def
       apply(auto simp add: vector_smult_assoc pth_3[symmetric]
         intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
-      by(auto simp add: neg_le_divide_eq neg_divide_le_eq real_mult_commute diff_le_iff)
+      by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff)
   }
   ultimately show ?thesis using False by auto
 qed
@@ -5723,7 +5723,7 @@
       thus ?thesis using `e>0` by auto
     next
       case False hence "d>0" unfolding d_def using zero_le_dist[of "z 0" "z 1"]
-        by (metis False d_def real_less_def)
+        by (metis False d_def less_le)
       hence "0 < e * (1 - c) / d" using `e>0` and `1-c>0`
         using divide_pos_pos[of "e * (1 - c)" d] and mult_pos_pos[of e "1 - c"] by auto
       then obtain N where N:"c ^ N < e * (1 - c) / d" using real_arch_pow_inv[of "e * (1 - c) / d" c] and c by auto
@@ -5731,18 +5731,18 @@
         have *:"c ^ n \<le> c ^ N" using `n\<ge>N` and c using power_decreasing[OF `n\<ge>N`, of c] by auto
         have "1 - c ^ (m - n) > 0" using c and power_strict_mono[of c 1 "m - n"] using `m>n` by auto
         hence **:"d * (1 - c ^ (m - n)) / (1 - c) > 0"
-          using real_mult_order[OF `d>0`, of "1 - c ^ (m - n)"]
+          using mult_pos_pos[OF `d>0`, of "1 - c ^ (m - n)"]
           using divide_pos_pos[of "d * (1 - c ^ (m - n))" "1 - c"]
           using `0 < 1 - c` by auto
 
         have "dist (z m) (z n) \<le> c ^ n * d * (1 - c ^ (m - n)) / (1 - c)"
           using cf_z2[of n "m - n"] and `m>n` unfolding pos_le_divide_eq[OF `1-c>0`]
-          by (auto simp add: real_mult_commute dist_commute)
+          by (auto simp add: mult_commute dist_commute)
         also have "\<dots> \<le> c ^ N * d * (1 - c ^ (m - n)) / (1 - c)"
           using mult_right_mono[OF * order_less_imp_le[OF **]]
-          unfolding real_mult_assoc by auto
+          unfolding mult_assoc by auto
         also have "\<dots> < (e * (1 - c) / d) * d * (1 - c ^ (m - n)) / (1 - c)"
-          using mult_strict_right_mono[OF N **] unfolding real_mult_assoc by auto
+          using mult_strict_right_mono[OF N **] unfolding mult_assoc by auto
         also have "\<dots> = e * (1 - c ^ (m - n))" using c and `d>0` and `1 - c > 0` by auto
         also have "\<dots> \<le> e" using c and `1 - c ^ (m - n) > 0` and `e>0` using mult_right_le_one_le[of e "1 - c ^ (m - n)"] by auto
         finally have  "dist (z m) (z n) < e" by auto
@@ -5770,7 +5770,7 @@
 
     have *:"c * dist (z N) x \<le> dist (z N) x" unfolding mult_le_cancel_right2
       using zero_le_dist[of "z N" x] and c
-      by (metis dist_eq_0_iff dist_nz order_less_asym real_less_def)
+      by (metis dist_eq_0_iff dist_nz order_less_asym less_le)
     have "dist (f (z N)) (f x) \<le> c * dist (z N) x" using lipschitz[THEN bspec[where x="z N"], THEN bspec[where x=x]]
       using z_in_s[of N] `x\<in>s` using c by auto
     also have "\<dots> < e / 2" using N' and c using * by auto
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
 
diff -r be5461582d0f -r 739a9379e29b src/HOL/Probability/Lebesgue.thy
--- a/src/HOL/Probability/Lebesgue.thy	Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/Probability/Lebesgue.thy	Sun May 09 22:51:11 2010 -0700
@@ -28,17 +28,17 @@
 lemma pos_neg_part_abs:
   fixes f :: "'a \<Rightarrow> real"
   shows "pos_part f x + neg_part f x = \<bar>f x\<bar>"
-unfolding real_abs_def pos_part_def neg_part_def by auto
+unfolding abs_if pos_part_def neg_part_def by auto
 
 lemma pos_part_abs:
   fixes f :: "'a \<Rightarrow> real"
   shows "pos_part (\<lambda> x. \<bar>f x\<bar>) y = \<bar>f y\<bar>"
-unfolding pos_part_def real_abs_def by auto
+unfolding pos_part_def abs_if by auto
 
 lemma neg_part_abs:
   fixes f :: "'a \<Rightarrow> real"
   shows "neg_part (\<lambda> x. \<bar>f x\<bar>) y = 0"
-unfolding neg_part_def real_abs_def by auto
+unfolding neg_part_def abs_if by auto
 
 lemma (in measure_space)
   assumes "f \<in> borel_measurable M"
@@ -341,7 +341,8 @@
   have "pos_simple_integral (k, c, (\<lambda> x. z x + z' x))
     = (\<Sum> x \<in> k. (z x + z' x) * measure M (c x))"
     unfolding pos_simple_integral_def by auto
-  also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x) + z' x * measure M (c x))" using real_add_mult_distrib by auto
+  also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x) + z' x * measure M (c x))"
+    by (simp add: left_distrib)
   also have "\<dots> = (\<Sum> x \<in> k. z x * measure M (c x)) + (\<Sum> x \<in> k. z' x * measure M (c x))" using setsum_addf by auto
   also have "\<dots> = pos_simple_integral (k, c, z) + pos_simple_integral (k, c, z')" unfolding pos_simple_integral_def by auto
   finally have ths: "pos_simple_integral (s, a, x) + pos_simple_integral (s', b, y) =
@@ -436,12 +437,12 @@
 lemma pos_simple_fn_integral_unique:
   assumes "(s, a, x) \<in> pos_simple f" "(s', b, y) \<in> pos_simple f"
   shows "pos_simple_integral (s, a, x) = pos_simple_integral (s', b, y)"
-using assms real_le_antisym real_le_refl pos_simple_integral_mono by metis
+using assms by (rule pos_simple_integral_equal) (* FIXME: redundant lemma *)
 
 lemma psfis_unique:
   assumes "a \<in> psfis f" "b \<in> psfis f"
   shows "a = b"
-using assms real_le_antisym real_le_refl psfis_mono by metis
+using assms by (intro order_antisym psfis_mono [OF _ _ order_refl])
 
 lemma pos_simple_integral_indicator:
   assumes "A \<in> sets M"
@@ -557,7 +558,7 @@
       using borel_measurable_indicator using sa'x[unfolded pos_simple_def] by auto
     hence "(\<lambda> w. x i * indicator_fn (a' i) w) \<in> borel_measurable M"
       using affine_borel_measurable[of "\<lambda> w. indicator_fn (a' i) w" 0 "x i"]
-        real_mult_commute by auto }
+        by (simp add: mult_commute) }
   from borel_measurable_setsum_borel_measurable[OF fs this] affine_borel_measurable
   have "(\<lambda> w. (\<Sum> i \<in> s. x i * indicator_fn (a' i) w)) \<in> borel_measurable M" by auto
   from borel_measurable_cong[OF pos_simple_setsum_indicator_fn[OF sa'x]] this
@@ -743,7 +744,7 @@
   assumes a: "a \<in> nnfis f" and b: "b \<in> nnfis f"
   shows "a = b"
   using nnfis_mono[OF a b] nnfis_mono[OF b a]
-  by (auto intro!: real_le_antisym[of a b])
+  by (auto intro!: order_antisym[of a b])
 
 lemma psfis_equiv:
   assumes "a \<in> psfis f" and "nonneg g"
@@ -843,7 +844,7 @@
       from nnfis this mono_convergent_le[OF mc]
       show "x n \<le> l" by (rule nnfis_mono)
     qed
-    ultimately have "l = z" by (rule real_le_antisym)
+    ultimately have "l = z" by (rule order_antisym)
     thus "c ----> z" using `c ----> l` by simp
   qed
 qed
@@ -859,7 +860,7 @@
     by auto
   thus "0 \<le> f x" using uy[rule_format]
     unfolding nnfis_def psfis_def pos_simple_def nonneg_def mono_convergent_def
-    using incseq_le[of "\<lambda> n. u n x" "f x"] real_le_trans
+    using incseq_le[of "\<lambda> n. u n x" "f x"] order_trans
     by fast
 qed
 
@@ -1335,10 +1336,10 @@
   also have "\<dots> \<le> integral (\<lambda> t. \<bar> f t \<bar> ^ n)"
     apply (rule integral_mono)
     using integral_cmul_indicator[OF w]
-      `integrable (\<lambda> x. \<bar>f x\<bar> ^ n)` real_le_trans[OF v1 v2] by auto
+      `integrable (\<lambda> x. \<bar>f x\<bar> ^ n)` order_trans[OF v1 v2] by auto
   finally show "measure M (f -` {a ..} \<inter> space M) \<le> integral (\<lambda>x. \<bar>f x\<bar>^n) / a^n"
     unfolding atLeast_def
-    by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: real_mult_commute)
+    by (auto intro!: mult_imp_le_div_pos[OF `0 < a ^ n`], simp add: mult_commute)
 qed
 
 lemma (in measure_space) integral_0:
diff -r be5461582d0f -r 739a9379e29b src/HOL/ex/Sqrt_Script.thy
--- a/src/HOL/ex/Sqrt_Script.thy	Sun May 09 17:47:43 2010 -0700
+++ b/src/HOL/ex/Sqrt_Script.thy	Sun May 09 22:51:11 2010 -0700
@@ -61,7 +61,7 @@
   apply (rule notI)
   apply (erule Rats_abs_nat_div_natE)
   apply (simp del: real_of_nat_mult
-              add: real_abs_def divide_eq_eq prime_not_square real_of_nat_mult [symmetric])
+              add: abs_if divide_eq_eq prime_not_square real_of_nat_mult [symmetric])
   done
 
 lemmas two_sqrt_irrational =