| changeset 44890 | 22f665a2e91c |
| parent 38353 | d98baa2cf589 |
| child 57442 | 2373b4c61111 |
--- a/src/HOL/Hoare/Arith2.thy Sun Sep 11 22:56:05 2011 +0200 +++ b/src/HOL/Hoare/Arith2.thy Mon Sep 12 07:55:43 2011 +0200 @@ -39,12 +39,12 @@ lemma cd_diff_l: "n<=m ==> cd x m n = cd x (m-n) n" apply (unfold cd_def) - apply (fastsimp dest: dvd_diffD) + apply (fastforce dest: dvd_diffD) done lemma cd_diff_r: "m<=n ==> cd x m n = cd x m (n-m)" apply (unfold cd_def) - apply (fastsimp dest: dvd_diffD) + apply (fastforce dest: dvd_diffD) done