doc-src/isac/jrocnik/Test_Integral.thy
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 13 Jul 2011 10:41:17 +0200
branchdecompose-isar
changeset 42081 b5a91fb4330c
permissions -rw-r--r--
started student work

for jrocnik: testfiles for integration, summation
for akargl, tleh: ml_quickstart, protocols
     1 (*
     2 doc-src/isac/jrocnik$ /usr/local/isabisac/bin/isabelle jedit Test_Integral.thy &
     3 *)
     4 
     5 theory Test_Integral imports "../../../src/HOL/Multivariate_Analysis/Integration"
     6 Integration begin
     7 
     8 ML {*
     9 @{term "Integral s f k"}
    10 *}
    11 ML {*
    12 *}
    13 ML {*
    14 *}
    15 
    16 end
    17