| author | Walther Neuper <neuper@ist.tugraz.at> |
| Fri, 22 Jul 2011 12:10:13 +0200 | |
| branch | decompose-isar |
| changeset 42164 | dc2fe21d2183 |
| parent 42081 | b5a91fb4330c |
| permissions | -rw-r--r-- |
| neuper@42081 | 1 |
(* |
| neuper@42081 | 2 |
doc-src/isac/jrocnik$ /usr/local/isabisac/bin/isabelle jedit Test_Integral.thy & |
| neuper@42081 | 3 |
*) |
| neuper@42081 | 4 |
|
| neuper@42081 | 5 |
theory Test_Integral imports "../../../src/HOL/Multivariate_Analysis/Integration" |
| neuper@42081 | 6 |
Integration begin |
| neuper@42081 | 7 |
|
| neuper@42081 | 8 |
ML {*
|
| neuper@42081 | 9 |
@{term "Integral s f k"}
|
| neuper@42081 | 10 |
*} |
| neuper@42081 | 11 |
ML {*
|
| neuper@42081 | 12 |
*} |
| neuper@42081 | 13 |
ML {*
|
| neuper@42081 | 14 |
*} |
| neuper@42081 | 15 |
|
| neuper@42081 | 16 |
end |
| neuper@42081 | 17 |