Nat.ML
changeset 233 f02021cf7cec
parent 218 78c9acf5bc38
child 239 e65129244146
--- a/Nat.ML	Wed Mar 15 10:44:26 1995 +0100
+++ b/Nat.ML	Fri Mar 17 15:48:55 1995 +0100
@@ -433,4 +433,4 @@
 by (simp_tac (nat_ss0 addsimps [le_eq_less_or_eq]) 1);
 qed "Suc_le_mono";
 
-val nat_ss = nat_ss0 addsimps [le_refl];
+val nat_ss = nat_ss0 addsimps [le_refl,Suc_le_mono];