src/Tools/isac/Interpret/Interpret.thy
author Walther Neuper <wneuper@ist.tugraz.at>
Wed, 30 Nov 2016 12:09:24 +0100
changeset 59263 0fde9446eda2
parent 59253 f0bb15a046ae
child 59279 255c853ea2f0
permissions -rw-r--r--
added structure Rtools : REWRITE_TOOLS
     1 (* Title:  collect all defitions for the Lucas-Interpreter
     2    Author: Walther Neuper 110226
     3    (c) due to copyright terms
     4  *)
     5 
     6 theory Interpret
     7 imports "~~/src/Tools/isac/ProgLang/ProgLang"
     8 begin
     9   ML_file "~~/src/Tools/isac/Interpret/mstools.sml"
    10   ML_file "~~/src/Tools/isac/Interpret/ctree.sml"
    11   ML_file "~~/src/Tools/isac/Interpret/ptyps.sml"
    12   ML_file "~~/src/Tools/isac/Interpret/generate.sml"
    13   ML_file "~~/src/Tools/isac/Interpret/calchead.sml"
    14   ML_file "~~/src/Tools/isac/Interpret/appl.sml"
    15   ML_file "~~/src/Tools/isac/Interpret/rewtools.sml"
    16   ML_file "~~/src/Tools/isac/Interpret/script.sml"
    17   ML_file "~~/src/Tools/isac/Interpret/solve.sml"
    18   ML_file "~~/src/Tools/isac/Interpret/inform.sml"
    19   ML_file "~~/src/Tools/isac/Interpret/mathengine.sml"
    20 (*declare [[ML_print_depth = 999]]*)
    21 ML {*
    22 *} ML {*
    23 *}
    24 end