1.1 --- a/src/HOL/Real/real_arith.ML	Mon Feb 16 15:24:03 2004 +0100
     1.2 +++ b/src/HOL/Real/real_arith.ML	Tue Feb 17 10:41:59 2004 +0100
     1.3 @@ -111,6 +111,8 @@
     1.4  val real_of_nat_le_zero_cancel_iff = thm "real_of_nat_le_zero_cancel_iff";
     1.5  val not_real_of_nat_less_zero = thm "not_real_of_nat_less_zero";
     1.6  val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff";
     1.7 +val real_number_of = thm"real_number_of";
     1.8 +val real_of_nat_number_of = thm"real_of_nat_number_of";
     1.9  
    1.10  
    1.11  (****Instantiation of the generic linear arithmetic package****)
    1.12 @@ -128,7 +130,8 @@
    1.13  val simps = [real_of_nat_zero, real_of_nat_Suc, real_of_nat_add, 
    1.14         real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add RS sym,
    1.15         real_of_int_minus RS sym, real_of_int_diff RS sym,
    1.16 -       real_of_int_mult RS sym];
    1.17 +       real_of_int_mult RS sym,
    1.18 +       real_of_nat_number_of, real_number_of];
    1.19  
    1.20  val int_inj_thms = [real_of_int_le_iff RS iffD2, real_of_int_less_iff RS iffD2,
    1.21                      real_of_int_inject RS iffD2];