# HG changeset patch
# User huffman
# Date 1315413939 25200
# Node ID 2690b6de5021490f19197ef84a5a68ba6f96a689
# Parent  a92f65e174cf3aa7d1f9490cfe102497455a0b48
remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq

diff -r a92f65e174cf -r 2690b6de5021 NEWS
--- 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
diff -r a92f65e174cf -r 2690b6de5021 src/HOL/RealDef.thy
--- 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]