diff -r 8aff580dce44 -r 6a82e122b337 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Tue Apr 23 17:25:29 1996 +0200
+++ b/src/HOL/Nat.ML	Tue Apr 23 17:34:05 1996 +0200
@@ -338,20 +338,19 @@
 qed "Suc_mono";
 
 
+(*
 goal Nat.thy "(Suc m < n | Suc m = n) = (m < n)";
 
 
 goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";
 by(stac less_Suc_eq 1);
 by(rtac 
-
+*)
 
-(*
 goal Nat.thy "(Suc(m) < Suc(n)) = (m<n)";
 by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]);
 qed "Suc_less_eq";
 Addsimps [Suc_less_eq];
-*)
 
 goal Nat.thy "~(Suc(n) < n)";
 by (fast_tac (HOL_cs addEs [Suc_lessD RS less_irrefl]) 1);