| changeset 9458 | c613cd06d5cf |
| parent 8745 | 13b32661dde4 |
| child 9541 | d17c0b34d5c8 |
| 9457:966974a7a5b3 | 9458:c613cd06d5cf |
|---|---|
19 and induction, for example |
19 and induction, for example |
20 *} |
20 *} |
21 |
21 |
22 lemma "sum n + sum n = n*(Suc n)"; |
22 lemma "sum n + sum n = n*(Suc n)"; |
23 apply(induct_tac n); |
23 apply(induct_tac n); |
24 apply(auto).; |
24 by(auto); |
25 |
25 |
26 (*<*) |
26 (*<*) |
27 end |
27 end |
28 (*>*) |
28 (*>*) |