Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Interpret/Interpret.thy
author Walther Neuper <wneuper@ist.tugraz.at>
Thu, 20 Oct 2016 10:26:29 +0200
changeset 59253 f0bb15a046ae
parent 59252 7d3dbc1171ff
child 59263 0fde9446eda2
permissions -rw-r--r--
simplify handling of theorems

Notes:
# this should complete 727dff4f6b2c
# see comment at "type thm''" (TODO: rename to thm')
# see comment at "type tac " at "| Rewrite"
!!! random errors *only* in test/../use-cases.sml
!!! probably due to "val states = Synchronized.var"
!!! see subsequent changeset for further hints. 
     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 ML {*

    21 *} ML {*

    22 *}

    23 end
wneuper/isa