# HG changeset patch
# User paulson
# Date 953727759 -3600
# Node ID 17325ee838ab2e5be8561dfa0c8373dfbab2e806
# Parent  ba33995b87ff7426b0184f67d440ee02dafbc2e9
Suc_less_eq now with AddIffs.  How could this have been overlooked?

diff -r ba33995b87ff -r 17325ee838ab src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Wed Mar 22 13:22:11 2000 +0100
+++ b/src/HOL/NatDef.ML	Wed Mar 22 13:22:39 2000 +0100
@@ -276,7 +276,7 @@
 Goal "(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];
+AddIffs [Suc_less_eq];
 
 (*Goal "~(Suc(n) < n)";
 by (blast_tac (claset() addEs [Suc_lessD RS less_irrefl]) 1);