author | wneuper <Walther.Neuper@jku.at> |
Sun, 09 Oct 2022 09:01:29 +0200 | |
changeset 60566 | 04f8699d2c9d |
parent 52107 | f8845fc8f38d |
permissions | -rwxr-xr-x |
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 {* |
jan@42276 | 17 |
val x = @{term "(SUM i = 0..< k. f i)"}; |
jan@42276 | 18 |
term2str x |
neuper@42164 | 19 |
*} |
neuper@42164 | 20 |
ML {* |
neuper@42081 | 21 |
*} |
neuper@42081 | 22 |
ML {* |
neuper@42081 | 23 |
*} |
neuper@42081 | 24 |
ML {* |
neuper@42081 | 25 |
*} |
neuper@42081 | 26 |
|
neuper@42081 | 27 |
end |
neuper@42081 | 28 |