| author | Walther Neuper <neuper@ist.tugraz.at> |
| Tue, 17 Sep 2013 09:50:52 +0200 | |
| changeset 52107 | f8845fc8f38d |
| parent 52056 | src/Doc/isac/jrocnik/Test_Integral.thy@f5d9bceb4dc0 |
| 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 |