src/HOL/Nat.ML
changeset 1672 2c109cd2fdd0
parent 1660 8cb42cd97579
child 1679 6a82e122b337
     1.1 --- a/src/HOL/Nat.ML	Tue Apr 23 16:44:22 1996 +0200
     1.2 +++ b/src/HOL/Nat.ML	Tue Apr 23 16:58:21 1996 +0200
     1.3 @@ -337,10 +337,21 @@
     1.4                       addEs  [less_trans, lessE]) 1);
     1.5  qed "Suc_mono";
     1.6  
     1.7 +
     1.8 +goal Nat.thy "(Suc m < n | Suc m = n) = (m < n)";
     1.9 +
    1.10 +
    1.11 +goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";
    1.12 +by(stac less_Suc_eq 1);
    1.13 +by(rtac 
    1.14 +
    1.15 +
    1.16 +(*
    1.17  goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";
    1.18  by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]);
    1.19  qed "Suc_less_eq";
    1.20  Addsimps [Suc_less_eq];
    1.21 +*)
    1.22  
    1.23  goal Nat.thy "~(Suc(n) < n)";
    1.24  by (fast_tac (HOL_cs addEs [Suc_lessD RS less_irrefl]) 1);