| author | Jan Rocnik <jan.rocnik@student.tugraz.at> |
| Tue, 27 Sep 2011 11:05:00 +0200 | |
| branch | decompose-isar |
| changeset 42293 | b24574463e1a |
| 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 |