remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq

--- a/NEWS	Wed Sep 07 09:02:58 2011 -0700
+++ b/NEWS	Wed Sep 07 09:45:39 2011 -0700
@@ -299,6 +299,7 @@
 * Complex_Main: Several redundant theorems have been removed or
 replaced by more general versions. INCOMPATIBILITY.
 
+  real_of_int_real_of_nat ~> real_of_int_of_nat_eq
   real_0_le_divide_iff ~> zero_le_divide_iff
   realpow_two_disj ~> power2_eq_iff
   real_squared_diff_one_factored ~> square_diff_one_factored

--- a/src/HOL/RealDef.thy	Wed Sep 07 09:02:58 2011 -0700
+++ b/src/HOL/RealDef.thy	Wed Sep 07 09:45:39 2011 -0700
@@ -1411,16 +1411,13 @@
 lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x" 
 by (insert real_of_nat_div2 [of n x], simp)
 
-lemma real_of_int_real_of_nat: "real (int n) = real n"
-by (simp add: real_of_nat_def real_of_int_def)
-
 lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n"
 by (simp add: real_of_int_def real_of_nat_def)
 
 lemma real_nat_eq_real [simp]: "0 <= x ==> real(nat x) = real x"
   apply (subgoal_tac "real(int(nat x)) = real(nat x)")
   apply force
-  apply (simp only: real_of_int_real_of_nat)
+  apply (simp only: real_of_int_of_nat_eq)
 done
 
 lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> Nats"
@@ -1534,7 +1531,7 @@
      "real (number_of v :: nat) =  
         (if neg (number_of v :: int) then 0  
          else (number_of v :: real))"
-by (simp add: real_of_int_real_of_nat [symmetric])
+by (simp add: real_of_int_of_nat_eq [symmetric])
 
 declaration {*
   K (Lin_Arith.add_inj_thms [@{thm real_of_nat_le_iff} RS iffD2, @{thm real_of_nat_inject} RS iffD2]