| changeset 30240 | 5b25fee0362c |
| parent 19802 | c2860c37e574 |
| child 33657 | a4179bf442d1 |
--- a/src/HOL/Hoare/Arith2.thy Wed Mar 04 10:43:39 2009 +0100 +++ b/src/HOL/Hoare/Arith2.thy Wed Mar 04 10:45:52 2009 +0100 @@ -42,12 +42,12 @@ lemma cd_diff_l: "n<=m ==> cd x m n = cd x (m-n) n" apply (unfold cd_def) - apply (blast intro: dvd_diff dest: dvd_diffD) + apply (fastsimp dest: dvd_diffD) done lemma cd_diff_r: "m<=n ==> cd x m n = cd x m (n-m)" apply (unfold cd_def) - apply (blast intro: dvd_diff dest: dvd_diffD) + apply (fastsimp dest: dvd_diffD) done