1.1 --- a/src/HOL/Integ/Int.ML	Mon Dec 31 14:13:07 2001 +0100
     1.2 +++ b/src/HOL/Integ/Int.ML	Wed Jan 02 16:06:31 2002 +0100
     1.3 @@ -356,11 +356,17 @@
     1.4  	      simpset() addsimps [neg_eq_less_0])); 
     1.5  qed "zless_nat_eq_int_zless";
     1.6  
     1.7 +Goal "0 <= z ==> int (nat z) = z"; 
     1.8 +by (asm_full_simp_tac
     1.9 +    (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); 
    1.10 +qed "nat_0_le"; 
    1.11 +
    1.12  Goal "z <= 0 ==> nat z = 0"; 
    1.13  by (auto_tac (claset(), 
    1.14  	      simpset() addsimps [order_le_less, neg_eq_less_0, 
    1.15  				  zle_def, neg_nat])); 
    1.16 -qed "nat_le_int0"; 
    1.17 +qed "nat_le_0"; 
    1.18 +Addsimps [nat_0_le, nat_le_0];
    1.19  
    1.20  (*An alternative condition is  0 <= w  *)
    1.21  Goal "0 < z ==> (nat w < nat z) = (w < z)";
    1.22 @@ -375,8 +381,7 @@
    1.23  
    1.24  Goal "(nat w < nat z) = (0 < z & w < z)";
    1.25  by (case_tac "0 < z" 1);
    1.26 -by (auto_tac (claset(), 
    1.27 -	      simpset() addsimps [lemma, nat_le_int0, linorder_not_less])); 
    1.28 +by (auto_tac (claset(), simpset() addsimps [lemma, linorder_not_less])); 
    1.29  qed "zless_nat_conj";
    1.30  
    1.31