# HG changeset patch
# User wenzelm
# Date 1001609123 -7200
# Node ID cd6d2eddf75f4d0fc8c7bec1ee87b92d7feb2b41
# Parent  fea20dc6b47018134c6262b5a3fed5ff11645451
renamed real_of_int_eq_iff to real_of_int_inject;

diff -r fea20dc6b470 -r cd6d2eddf75f src/HOL/Real/RealBin.ML
--- a/src/HOL/Real/RealBin.ML	Thu Sep 27 18:44:30 2001 +0200
+++ b/src/HOL/Real/RealBin.ML	Thu Sep 27 18:45:23 2001 +0200
@@ -82,7 +82,7 @@
 \     iszero (number_of (bin_add v (bin_minus v')))";
 by (simp_tac
     (HOL_ss addsimps [real_number_of_def, 
-	              real_of_int_eq_iff, eq_number_of_eq]) 1);
+	              real_of_int_inject, eq_number_of_eq]) 1);
 qed "eq_real_number_of";
 
 Addsimps [eq_real_number_of];
diff -r fea20dc6b470 -r cd6d2eddf75f src/HOL/Real/RealInt.ML
--- a/src/HOL/Real/RealInt.ML	Thu Sep 27 18:44:30 2001 +0200
+++ b/src/HOL/Real/RealInt.ML	Thu Sep 27 18:45:23 2001 +0200
@@ -114,8 +114,8 @@
 
 Goal "(real (x::int) = real y) = (x = y)";
 by (blast_tac (claset() addSDs [inj_real_of_int RS injD]) 1);
-qed "real_of_int_eq_iff";
-AddIffs [real_of_int_eq_iff];
+qed "real_of_int_inject";
+AddIffs [real_of_int_inject];
 
 Goal "x < y ==> (real (x::int) < real y)";
 by (full_simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);