changeset 5591 | fbb4e1ac234d |
parent 5553 | ae42b36a50c2 |
child 5771 | 7c2c8cf20221 |
--- a/src/HOL/arith_data.ML Thu Oct 01 18:22:24 1998 +0200 +++ b/src/HOL/arith_data.ML Thu Oct 01 18:23:00 1998 +0200 @@ -230,5 +230,5 @@ by (Clarify_tac 2); by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 2); by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans, - Suc_diff_le]) 1); + Suc_diff_le, less_imp_le]) 1); qed_spec_mp "diff_less_mono2";