changeset 962 | 136308504cd9 |
parent 923 | ff1574a81019 |
child 972 | e61b058d58d2 |
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];