src/HOL/Nat.ML
changeset 12949 b94843ffc0d1
parent 12931 2c0251fada94
child 13094 643fce75f6cd
     1.1 --- a/src/HOL/Nat.ML	Tue Feb 26 12:51:40 2002 +0100
     1.2 +++ b/src/HOL/Nat.ML	Tue Feb 26 13:37:48 2002 +0100
     1.3 @@ -258,19 +258,6 @@
     1.4                                   delsimps [add_0_right]) 1);
     1.5  qed "add_eq_self_zero";
     1.6  
     1.7 -(* a rather special thm needed for arith_tac: m+n = 0 may arise where m or n
     1.8 -contain Suc. This contradiction must be detected. It cannot be detected by
     1.9 -pulling Suc outside because this interferes with simprocs on
    1.10 -numerals. Sigh. *)
    1.11 -
    1.12 -Goal "m ~= 0 ==> m+n ~= (0::nat)";
    1.13 -by(Asm_full_simp_tac 1);
    1.14 -qed "add_not_0_if_left_not_0";
    1.15 -
    1.16 -Goal "n ~= 0 ==> m+n ~= (0::nat)";
    1.17 -by(Asm_full_simp_tac 1);
    1.18 -qed "add_not_0_if_right_not_0";
    1.19 -
    1.20  (**** Additional theorems about "less than" ****)
    1.21  
    1.22  (*Deleted less_natE; instead use less_imp_Suc_add RS exE*)