# HG changeset patch
# User paulson
# Date 835259173 -7200
# Node ID 3994d37b16ae58707e3b8b3ad776de26bff88971
# Parent  b03dba9116d431d00181c29910b1fa21161c3d05
Corrected comment

diff -r b03dba9116d4 -r 3994d37b16ae src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Tue Jun 18 16:38:48 1996 +0200
+++ b/src/HOL/Nat.ML	Thu Jun 20 10:26:13 1996 +0200
@@ -242,7 +242,7 @@
 by (etac (wf_pred_nat RS wf_trancl RS wf_irrefl) 1);
 qed "less_not_refl";
 
-(* n(n ==> R *)
+(* n<n ==> R *)
 bind_thm ("less_irrefl", (less_not_refl RS notE));
 
 goal Nat.thy "!!m. n<m ==> m ~= (n::nat)";
@@ -457,6 +457,18 @@
 by (Fast_tac 1);
 qed "Suc_leD";
 
+(* stronger version of Suc_leD *)
+goalw Nat.thy [le_def] 
+        "!!m. Suc m <= n ==> m < n";
+by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
+by (cut_facts_tac [less_linear] 1);
+by (fast_tac HOL_cs 1);
+qed "Suc_le_lessD";
+
+goal Nat.thy "(Suc m <= n) = (m < n)";
+by (fast_tac (!claset addIs [lessD, Suc_le_lessD]) 1);
+qed "Suc_le_eq";
+
 goalw Nat.thy [le_def] "!!m. m <= n ==> m <= Suc n";
 by (fast_tac (!claset addDs [Suc_lessD]) 1);
 qed "le_SucI";