--- a/src/HOL/Real/real_arith.ML Thu Jul 14 14:05:48 2005 +0200
+++ b/src/HOL/Real/real_arith.ML Thu Jul 14 17:16:52 2005 +0200
@@ -99,9 +99,9 @@
local
val simps = [real_of_nat_zero, real_of_nat_Suc, real_of_nat_add,
- real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add RS sym,
- real_of_int_minus RS sym, real_of_int_diff RS sym,
- real_of_int_mult RS sym, real_of_int_of_nat_eq,
+ real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add,
+ real_of_int_minus, real_of_int_diff,
+ real_of_int_mult, real_of_int_of_nat_eq,
real_of_nat_number_of, real_number_of];
val int_inj_thms = [real_of_int_le_iff RS iffD2, real_of_int_less_iff RS iffD2,