src/HOL/Nat.ML
changeset 5644 85fd64148873
parent 5316 7a8975451a89
child 5983 79e301a6a51b
     1.1 --- a/src/HOL/Nat.ML	Tue Oct 13 14:25:01 1998 +0200
     1.2 +++ b/src/HOL/Nat.ML	Wed Oct 14 11:50:48 1998 +0200
     1.3 @@ -38,6 +38,12 @@
     1.4  qed "neq0_conv";
     1.5  AddIffs [neq0_conv];
     1.6  
     1.7 +Goal "(0 ~= n) = (0 < n)";
     1.8 +by(exhaust_tac "n" 1);
     1.9 +by(Auto_tac);
    1.10 +qed "zero_neq_conv";
    1.11 +AddIffs [zero_neq_conv];
    1.12 +
    1.13  (*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
    1.14  bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
    1.15