--- a/src/HOL/Real/real_arith.ML Mon Feb 16 15:24:03 2004 +0100
+++ b/src/HOL/Real/real_arith.ML Tue Feb 17 10:41:59 2004 +0100
@@ -111,6 +111,8 @@
val real_of_nat_le_zero_cancel_iff = thm "real_of_nat_le_zero_cancel_iff";
val not_real_of_nat_less_zero = thm "not_real_of_nat_less_zero";
val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff";
+val real_number_of = thm"real_number_of";
+val real_of_nat_number_of = thm"real_of_nat_number_of";
(****Instantiation of the generic linear arithmetic package****)
@@ -128,7 +130,8 @@
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_mult RS sym,
+ 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,
real_of_int_inject RS iffD2];