| changeset 15439 | 71c0f98e31f1 |
| parent 15404 | a9a762f586b5 |
| child 15539 | 333a88244569 |
--- a/src/HOL/NatArith.thy Thu Jan 13 14:56:37 2005 +0100 +++ b/src/HOL/NatArith.thy Fri Jan 14 12:00:27 2005 +0100 @@ -62,7 +62,7 @@ (*Replaces the previous diff_less and le_diff_less, which had the stronger second premise n\<le>m*) -lemma diff_less: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m" +lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m" by arith