doc-src/isac/jrocnik/Test_Integral.thy
author Jan Rocnik <jan.rocnik@student.tugraz.at>
Thu, 08 Sep 2011 23:17:35 +0200
branchdecompose-isar
changeset 42252 e633bb41ea42
parent 42081 b5a91fb4330c
permissions -rw-r--r--
setted up envoirement for latex includement (tuned)
     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