src/HOL/Nat.ML
changeset 8115 c802042066e8
parent 7089 9bfb8e218b99
child 8260 87f21e25fcb6
     1.1 --- a/src/HOL/Nat.ML	Fri Jan 07 11:06:03 2000 +0100
     1.2 +++ b/src/HOL/Nat.ML	Mon Jan 10 16:06:43 2000 +0100
     1.3 @@ -46,6 +46,10 @@
     1.4  (*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
     1.5  bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
     1.6  
     1.7 +Goal "(0<n) = (EX m. n = Suc m)";
     1.8 +by(fast_tac (claset() addIs [not0_implies_Suc]) 1);
     1.9 +qed "gr0_conv_Suc";
    1.10 +
    1.11  Goal "(~(0 < n)) = (n=0)";
    1.12  by (rtac iffI 1);
    1.13   by (etac swap 1);