| author | Walther Neuper <neuper@ist.tugraz.at> |
| Sun, 14 Jul 2013 14:48:14 +0200 | |
| changeset 52056 | f5d9bceb4dc0 |
| parent 42276 | doc-src/isac/jrocnik/Test_SUM.thy@8d642a598ca3 |
| permissions | -rwxr-xr-x |
2 theory Test_SUM imports Isac begin
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 *}
27 end