# HG changeset patch
# User paulson
# Date 932390970 -7200
# Node ID 99e012d61eef1cc0f37774a1e80955886f10fa10
# Parent  c7479ae352b10491d5cb0e835948fdcf8eef1876
new theorem zless_zero_nat

diff -r c7479ae352b1 -r 99e012d61eef src/HOL/Integ/Int.ML
--- a/src/HOL/Integ/Int.ML	Mon Jul 19 15:29:01 1999 +0200
+++ b/src/HOL/Integ/Int.ML	Mon Jul 19 15:29:30 1999 +0200
@@ -253,6 +253,12 @@
 	      simpset() addsimps [lemma, nat_le_int0, linorder_not_less])); 
 qed "zless_nat_conj";
 
+Goal "(0 < nat z) = (int 0 < z)";
+by (stac (order_refl RS nat_le_int0 RS sym) 1);
+by (stac (zless_nat_conj) 1);
+by (Simp_tac 1);
+qed "zless_zero_nat";
+
 
 (* a case theorem distinguishing non-negative and negative int *)