| changeset 12815 | 1f073030b97a |
| parent 11494 | 23a118849801 |
| child 17914 | 99ead7a7eb42 |
| 12814:2f5edb146f7e | 12815:1f073030b97a |
|---|---|
47 We do not show the proof script. |
47 We do not show the proof script. |
48 *} |
48 *} |
49 (*<*) |
49 (*<*) |
50 apply simp |
50 apply simp |
51 apply simp |
51 apply simp |
52 apply(simp add:dvd_def) |
52 apply(simp add: dvd_def) |
53 apply(clarify) |
53 apply(clarify) |
54 apply(rule_tac x = "Suc k" in exI) |
54 apply(rule_tac x = "Suc k" in exI) |
55 apply simp |
55 apply simp |
56 done |
56 done |
57 (*>*) |
57 (*>*) |