# HG changeset patch
# User lcp
# Date 793902033 -3600
# Node ID 78c9acf5bc38962f3953cafe74fb69fa05adc3a6
# Parent  b6c0407f203e716e48cf78a9481b76ffdf420c3e
Moved succ_leq_mono from IOA/example/Lemmas to Nat.ML as Suc_le_mono.
Moved less_leq_less from IOA/example/Lemmas to Nat.ML as less_le_trans.

diff -r b6c0407f203e -r 78c9acf5bc38 Nat.ML
--- a/Nat.ML	Mon Feb 27 16:46:38 1995 +0100
+++ b/Nat.ML	Mon Feb 27 17:20:33 1995 +0100
@@ -414,6 +414,11 @@
 by (fast_tac (HOL_cs addIs [less_trans]) 1);
 qed "le_less_trans";
 
+goal Nat.thy "!!i. [| i < j; j <= k |] ==> i < (k::nat)";
+by (dtac le_imp_less_or_eq 1);
+by (fast_tac (HOL_cs addIs [less_trans]) 1);
+qed "less_le_trans";
+
 goal Nat.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)";
 by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
           rtac less_or_eq_imp_le, fast_tac (HOL_cs addIs [less_trans])]);
@@ -424,4 +429,8 @@
           fast_tac (HOL_cs addEs [less_anti_refl,less_asym])]);
 qed "le_anti_sym";
 
+goal Nat.thy "(Suc(n) <= Suc(m)) = (n <= m)";
+by (simp_tac (nat_ss0 addsimps [le_eq_less_or_eq]) 1);
+qed "Suc_le_mono";
+
 val nat_ss = nat_ss0 addsimps [le_refl];