src/HOL/Real/real_arith.ML
changeset 14390 55fe71faadda
parent 14387 e96d5c42c4b0
child 14426 de890c247b38
--- 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];