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.
neuper@41905
     1
(* Title:  collect all defitions for the Lucas-Interpreter
neuper@41905
     2
   Author: Walther Neuper 110226
neuper@41905
     3
   (c) due to copyright terms
neuper@41905
     4
 *)
neuper@41905
     5
neuper@48761
     6
theory Interpret
neuper@48880
     7
imports "~~/src/Tools/isac/ProgLang/ProgLang"
neuper@41905
     8
begin
neuper@55275
     9
  ML_file "~~/src/Tools/isac/Interpret/mstools.sml"
neuper@55275
    10
  ML_file "~~/src/Tools/isac/Interpret/ctree.sml"
neuper@55275
    11
  ML_file "~~/src/Tools/isac/Interpret/ptyps.sml"
neuper@55275
    12
  ML_file "~~/src/Tools/isac/Interpret/generate.sml"
neuper@55275
    13
  ML_file "~~/src/Tools/isac/Interpret/calchead.sml"
neuper@55275
    14
  ML_file "~~/src/Tools/isac/Interpret/appl.sml"
neuper@55275
    15
  ML_file "~~/src/Tools/isac/Interpret/rewtools.sml"
neuper@55275
    16
  ML_file "~~/src/Tools/isac/Interpret/script.sml"
neuper@55275
    17
  ML_file "~~/src/Tools/isac/Interpret/solve.sml"
neuper@55275
    18
  ML_file "~~/src/Tools/isac/Interpret/inform.sml"
neuper@55275
    19
  ML_file "~~/src/Tools/isac/Interpret/mathengine.sml"
wneuper@59250
    20
ML {*
wneuper@59250
    21
*} ML {*
wneuper@59250
    22
*}
neuper@41905
    23
end