author | paulson |
Tue, 01 Sep 1998 15:05:36 +0200 | |
changeset 5418 | a895ab904b85 |
parent 5417 | 1f533238b53b |
child 5419 | 3a744748dd21 |
--- a/src/HOL/arith_data.ML Tue Sep 01 15:04:59 1998 +0200 +++ b/src/HOL/arith_data.ML Tue Sep 01 15:05:36 1998 +0200 @@ -228,7 +228,7 @@ by (Clarify_tac 1); by (etac less_SucE 1); by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans, - Suc_diff_n]) 1); + Suc_diff_le]) 1); by (Clarify_tac 1); by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 1); qed_spec_mp "diff_less_mono2";