src/HOL/Nat.ML
changeset 1679 6a82e122b337
parent 1672 2c109cd2fdd0
child 1760 6f41a494f3b1
     1.1 --- a/src/HOL/Nat.ML	Tue Apr 23 17:25:29 1996 +0200
     1.2 +++ b/src/HOL/Nat.ML	Tue Apr 23 17:34:05 1996 +0200
     1.3 @@ -338,20 +338,19 @@
     1.4  qed "Suc_mono";
     1.5  
     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 -(*
    1.18  goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";
    1.19  by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]);
    1.20  qed "Suc_less_eq";
    1.21  Addsimps [Suc_less_eq];
    1.22 -*)
    1.23  
    1.24  goal Nat.thy "~(Suc(n) < n)";
    1.25  by (fast_tac (HOL_cs addEs [Suc_lessD RS less_irrefl]) 1);