1.1 --- a/src/HOL/Nat.ML	Fri Mar 17 15:35:09 1995 +0100
     1.2 +++ b/src/HOL/Nat.ML	Fri Mar 17 15:49:37 1995 +0100
     1.3 @@ -433,4 +433,4 @@
     1.4  by (simp_tac (nat_ss0 addsimps [le_eq_less_or_eq]) 1);
     1.5  qed "Suc_le_mono";
     1.6  
     1.7 -val nat_ss = nat_ss0 addsimps [le_refl];
     1.8 +val nat_ss = nat_ss0 addsimps [le_refl,Suc_le_mono];