# HG changeset patch
# User paulson
# Date 887102818 -3600
# Node ID 122015efd4e1e8a32659be5ad473f8d804185d40
# Parent  67a726003cf89df540b6263dc24b316fcd955008
New AddIffs le_0_eq and neq0_conv

diff -r 67a726003cf8 -r 122015efd4e1 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Mon Feb 09 18:09:35 1998 +0100
+++ b/src/HOL/NatDef.ML	Tue Feb 10 10:26:58 1998 +0100
@@ -300,8 +300,8 @@
 by (etac ssubst 1);
 by (rtac zero_less_Suc 1);
 qed "neq0_conv";
-Addsimps [neq0_conv];
-AddSDs [neq0_conv RS iffD1];
+AddIffs [neq0_conv];
+
 
 bind_thm("gr0I", notI RS (neq0_conv RS iffD1));
 
@@ -437,6 +437,7 @@
 by (nat_ind_tac "i" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "le_0_eq";
+AddIffs [le_0_eq];
 
 Addsimps [(*less_Suc_eq, makes simpset non-confluent*) le0, le_0_eq,
           Suc_n_not_le_n,
@@ -448,6 +449,9 @@
 by (blast_tac (claset() addSEs [less_SucE] addIs [less_SucI]) 1);
 qed "le_Suc_eq";
 
+(* [| m <= Suc n;  m <= n ==> R;  m = Suc n ==> R |] ==> R *)
+bind_thm ("le_SucE", le_Suc_eq RS iffD1 RS disjE);
+
 (*
 goal thy "(Suc m < n | Suc m = n) = (m < n)";
 by (stac (less_Suc_eq RS sym) 1);