1.1 --- a/src/HOL/Real/RealInt.ML	Mon Dec 31 14:13:07 2001 +0100
     1.2 +++ b/src/HOL/Real/RealInt.ML	Wed Jan 02 16:06:31 2002 +0100
     1.3 @@ -39,12 +39,13 @@
     1.4  by (simp_tac (simpset() addsimps [real_of_int, preal_add_commute]) 1);
     1.5  qed "real_of_int_zero";
     1.6  
     1.7 -Goalw [int_def,real_one_def] "real (int 1) = (1::real)";
     1.8 +Goal "real (1::int) = (1::real)";
     1.9 +by (stac (int_1 RS sym) 1); 
    1.10  by (auto_tac (claset(),
    1.11 -	      simpset() addsimps [real_of_int,
    1.12 -				  preal_of_prat_add RS sym,pnat_two_eq,
    1.13 -			       prat_of_pnat_add RS sym,pnat_one_iff RS sym]));
    1.14 -qed "real_of_int_one";
    1.15 +	      simpset() addsimps [int_def, real_one_def, real_of_int,
    1.16 +			       preal_of_prat_add RS sym,pnat_two_eq,
    1.17 +			       prat_of_pnat_add RS sym, pnat_one_iff RS sym]));
    1.18 +qed "real_of_one";
    1.19  
    1.20  Goal "real (x::int) + real y = real (x + y)";
    1.21  by (res_inst_tac [("z","x")] eq_Abs_Integ 1);
    1.22 @@ -81,7 +82,7 @@
    1.23  Addsimps [real_of_int_mult RS sym];
    1.24  
    1.25  Goal "real (int (Suc n)) = real (int n) + (1::real)";
    1.26 -by (simp_tac (simpset() addsimps [real_of_int_one RS sym, zadd_int] @ 
    1.27 +by (simp_tac (simpset() addsimps [real_of_one RS sym, zadd_int] @ 
    1.28                                   zadd_ac) 1);
    1.29  qed "real_of_int_Suc";
    1.30  
    1.31 @@ -133,3 +134,6 @@
    1.32  by (full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
    1.33  qed "real_of_int_le_iff";
    1.34  Addsimps [real_of_int_le_iff];
    1.35 +
    1.36 +Addsimps [real_of_one];
    1.37 +