diff -r 09a7a180cc99 -r c802042066e8 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Fri Jan 07 11:06:03 2000 +0100
+++ b/src/HOL/Nat.ML	Mon Jan 10 16:06:43 2000 +0100
@@ -46,6 +46,10 @@
 (*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
 bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
 
+Goal "(0<n) = (EX m. n = Suc m)";
+by(fast_tac (claset() addIs [not0_implies_Suc]) 1);
+qed "gr0_conv_Suc";
+
 Goal "(~(0 < n)) = (n=0)";
 by (rtac iffI 1);
  by (etac swap 1);