| branch | decompose-isar |
| changeset 42276 | 8d642a598ca3 |
| parent 42164 | dc2fe21d2183 |
| 42275:9f6d15630042 | 42276:8d642a598ca3 |
|---|---|
12 @{term "(%n. n+n) a"}; |
12 @{term "(%n. n+n) a"}; |
13 @{term "a+a"}; |
13 @{term "a+a"}; |
14 *} |
14 *} |
15 section {*sums*} |
15 section {*sums*} |
16 ML {* |
16 ML {* |
17 @{term "(SUM i = 0..< k. f i)"} |
17 val x = @{term "(SUM i = 0..< k. f i)"}; |
18 term2str x |
|
18 *} |
19 *} |
19 ML {* |
20 ML {* |
20 *} |
21 *} |
21 ML {* |
22 ML {* |
22 *} |
23 *} |