src/Tools/isac/Interpret/Interpret.thy
author Walther Neuper <neuper@ist.tugraz.at>
Fri, 12 Oct 2012 17:06:58 +0200
changeset 48761 4162c4f6f897
parent 41943 f33f6959948b
child 48880 ea0c337066d9
permissions -rw-r--r--
2011-->2012: ProofContext-->Proof_Context

once more; was reverted before
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@48761
     7
imports "../ProgLang/ProgLang"
neuper@48761
     8
uses ("mstools.sml") ("ctree.sml") ("ptyps.sml") ("generate.sml")
neuper@48761
     9
     ("calchead.sml") ("appl.sml") ("rewtools.sml") ("script.sml")
neuper@48761
    10
     ("solve.sml") ("inform.sml") ("mathengine.sml")
neuper@41905
    11
begin
neuper@41905
    12
neuper@41905
    13
  use "mstools.sml"
neuper@41905
    14
  use "ctree.sml"
neuper@41905
    15
  use "ptyps.sml"
neuper@41905
    16
  use "generate.sml"
neuper@41905
    17
  use "calchead.sml"
neuper@41905
    18
  use "appl.sml"
neuper@41905
    19
  use "rewtools.sml"
neuper@41905
    20
  use "script.sml"
neuper@41905
    21
  use "solve.sml"
neuper@41905
    22
  use "inform.sml"
neuper@41905
    23
  use "mathengine.sml"
neuper@41905
    24
neuper@41905
    25
end