| author | Jan Rocnik <jan.rocnik@student.tugraz.at> |
| Tue, 06 Sep 2011 15:57:25 +0200 | |
| branch | decompose-isar |
| changeset 42245 | 3d1f27a0f8a4 |
| parent 42164 | dc2fe21d2183 |
| child 42276 | 8d642a598ca3 |
| permissions | -rw-r--r-- |
| neuper@42081 | 1 |
|
| neuper@42081 | 2 |
theory Test_SUM imports Isac begin |
| neuper@42081 | 3 |
|
| neuper@42164 | 4 |
section {*trials with implicit function, probably required*}
|
| neuper@42160 | 5 |
ML {*
|
| neuper@42160 | 6 |
@{term "(%n :: nat. n) 2"};
|
| neuper@42160 | 7 |
@{term "(%n. n) 2"};
|
| neuper@42160 | 8 |
@{term "2"};
|
| neuper@42160 | 9 |
*} |
| neuper@42160 | 10 |
ML {*
|
| neuper@42160 | 11 |
@{term "(%n. n+n)"};
|
| neuper@42160 | 12 |
@{term "(%n. n+n) a"};
|
| neuper@42160 | 13 |
@{term "a+a"};
|
| neuper@42160 | 14 |
*} |
| neuper@42164 | 15 |
section {*sums*}
|
| neuper@42160 | 16 |
ML {*
|
| neuper@42164 | 17 |
@{term "(SUM i = 0..< k. f i)"}
|
| neuper@42164 | 18 |
*} |
| neuper@42164 | 19 |
ML {*
|
| neuper@42081 | 20 |
*} |
| neuper@42081 | 21 |
ML {*
|
| neuper@42081 | 22 |
*} |
| neuper@42081 | 23 |
ML {*
|
| neuper@42081 | 24 |
*} |
| neuper@42081 | 25 |
|
| neuper@42081 | 26 |
end |
| neuper@42081 | 27 |