changeset 52056 | f5d9bceb4dc0 |
parent 42276 | 8d642a598ca3 |
48899:79e5b6eec425 | 52056:f5d9bceb4dc0 |
---|---|
1 |
|
2 theory Test_SUM imports Isac begin |
|
3 |
|
4 section {*trials with implicit function, probably required*} |
|
5 ML {* |
|
6 @{term "(%n :: nat. n) 2"}; |
|
7 @{term "(%n. n) 2"}; |
|
8 @{term "2"}; |
|
9 *} |
|
10 ML {* |
|
11 @{term "(%n. n+n)"}; |
|
12 @{term "(%n. n+n) a"}; |
|
13 @{term "a+a"}; |
|
14 *} |
|
15 section {*sums*} |
|
16 ML {* |
|
17 val x = @{term "(SUM i = 0..< k. f i)"}; |
|
18 term2str x |
|
19 *} |
|
20 ML {* |
|
21 *} |
|
22 ML {* |
|
23 *} |
|
24 ML {* |
|
25 *} |
|
26 |
|
27 end |
|
28 |