src/HOL/Nat.ML
changeset 1672 2c109cd2fdd0
parent 1660 8cb42cd97579
child 1679 6a82e122b337
--- a/src/HOL/Nat.ML	Tue Apr 23 16:44:22 1996 +0200
+++ b/src/HOL/Nat.ML	Tue Apr 23 16:58:21 1996 +0200
@@ -337,10 +337,21 @@
                      addEs  [less_trans, lessE]) 1);
 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);