src/HOL/Real/RealInt.ML
changeset 13849 2584233cf3ef
parent 12613 279facb4253a
     1.1 --- a/src/HOL/Real/RealInt.ML	Thu Mar 06 12:22:28 2003 +0100
     1.2 +++ b/src/HOL/Real/RealInt.ML	Thu Mar 06 15:02:51 2003 +0100
     1.3 @@ -95,8 +95,7 @@
     1.4  qed "real_of_int_real_of_nat";
     1.5  
     1.6  Goal "~neg z ==> real (nat z) = real z";
     1.7 -by (asm_simp_tac (simpset() addsimps [not_neg_nat,
     1.8 -				      real_of_int_real_of_nat RS sym]) 1);
     1.9 +by (asm_full_simp_tac (simpset() addsimps [not_neg_eq_ge_0, real_of_int_real_of_nat RS sym]) 1);
    1.10  qed "real_of_nat_real_of_int";
    1.11  
    1.12  Goal "(real x = 0) = (x = int 0)";