1.1 --- a/src/HOL/Integ/int_arith2.ML	Mon Dec 31 14:13:07 2001 +0100
     1.2 +++ b/src/HOL/Integ/int_arith2.ML	Wed Jan 02 16:06:31 2002 +0100
     1.3 @@ -21,20 +21,6 @@
     1.4  
     1.5  (* nat *)
     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 (case_tac "z = 0" 1);
    1.14 -by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1); 
    1.15 -by (asm_full_simp_tac 
    1.16 -    (simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1);
    1.17 -qed "nat_le_0"; 
    1.18 -
    1.19 -Addsimps [nat_0_le, nat_le_0];
    1.20 -
    1.21  val [major,minor] = Goal "[| 0 <= z;  !!m. z = int m ==> P |] ==> P"; 
    1.22  by (rtac (major RS nat_0_le RS sym RS minor) 1);
    1.23  qed "nonneg_eq_int";