# HG changeset patch
# User paulson
# Date 887969271 -3600
# Node ID c448e09d0fca652cd521e1babc166f1ce6746e25
# Parent  83d364462ce16477c79c3060eb964b277f092862
New theorem eq_imp_le

diff -r 83d364462ce1 -r c448e09d0fca src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Thu Feb 19 15:01:25 1998 +0100
+++ b/src/HOL/NatDef.ML	Fri Feb 20 11:07:51 1998 +0100
@@ -302,8 +302,8 @@
 qed "neq0_conv";
 AddIffs [neq0_conv];
 
-
-bind_thm("gr0I", notI RS (neq0_conv RS iffD1));
+(*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
+bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
 
 goal thy "(~(0 < n)) = (n=0)";
 by (rtac iffI 1);
@@ -545,6 +545,9 @@
 by (REPEAT(ares_tac [iffI,less_or_eq_imp_le,le_imp_less_or_eq] 1));
 qed "le_eq_less_or_eq";
 
+(*Useful with Blast_tac.   m=n ==> m<=n *)
+bind_thm ("eq_imp_le", disjI2 RS less_or_eq_imp_le);
+
 goal thy "n <= (n::nat)";
 by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
 qed "le_refl";