1.1 --- a/src/HOL/NatDef.ML	Wed Mar 22 13:22:11 2000 +0100
     1.2 +++ b/src/HOL/NatDef.ML	Wed Mar 22 13:22:39 2000 +0100
     1.3 @@ -276,7 +276,7 @@
     1.4  Goal "(Suc(m) < Suc(n)) = (m<n)";
     1.5  by (EVERY1 [rtac iffI, etac Suc_less_SucD, etac Suc_mono]);
     1.6  qed "Suc_less_eq";
     1.7 -Addsimps [Suc_less_eq];
     1.8 +AddIffs [Suc_less_eq];
     1.9  
    1.10  (*Goal "~(Suc(n) < n)";
    1.11  by (blast_tac (claset() addEs [Suc_lessD RS less_irrefl]) 1);