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];