| author | Jan Rocnik <jan.rocnik@student.tugraz.at> |
| Thu, 08 Sep 2011 23:17:35 +0200 | |
| branch | decompose-isar |
| changeset 42252 | e633bb41ea42 |
| parent 42164 | dc2fe21d2183 |
| child 42276 | 8d642a598ca3 |
| permissions | -rw-r--r-- |
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 @{term "(SUM i = 0..< k. f i)"}
18 *}
19 ML {*
20 *}
21 ML {*
22 *}
23 ML {*
24 *}
26 end