src/HOL/Real/RealOrd.ML
changeset 10043 a0364652e115
parent 9825 a0fcf6f0436c
child 10606 e3229a37d53f
     1.1 --- a/src/HOL/Real/RealOrd.ML	Thu Sep 21 10:42:49 2000 +0200
     1.2 +++ b/src/HOL/Real/RealOrd.ML	Thu Sep 21 12:11:38 2000 +0200
     1.3 @@ -428,6 +428,12 @@
     1.4  qed "real_of_posnat_rinv_gt_zero";
     1.5  Addsimps [real_of_posnat_rinv_gt_zero];
     1.6  
     1.7 +Goal "real_of_preal (preal_of_prat (prat_of_pnat (pnat_of_nat N))) = \
     1.8 +\     real_of_nat (Suc N)";
     1.9 +by (simp_tac (simpset() addsimps [real_of_nat_def,real_of_posnat_Suc,
    1.10 +    real_add_assoc,(real_of_posnat_def RS meta_eq_to_obj_eq) RS sym]) 1);
    1.11 +qed "real_of_preal_real_of_nat_Suc";
    1.12 +
    1.13  Goal "x+x = x*(1r+1r)";
    1.14  by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
    1.15  qed "real_add_self";