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 <neuper@ist.tugraz.at>
Sun, 16 Jun 2013 12:31:41 +0200
changeset 48880 ea0c337066d9
parent 48761 4162c4f6f897
child 55275 f08422eeef24
permissions -rw-r--r--
Isabelle2011 --> 2012 intermediate

Made paths absolute wrt ~~, which probably will be shortened later again.
'isabelle usedir -b HOL Isac' successfully creates a heap;
still no 'thehier' created in 'Knowledge/Build_Thydata.thy',
because these are not required by the math-engine. 
     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 uses 

     9   ("~~/src/Tools/isac/Interpret/mstools.sml") 

    10   ("~~/src/Tools/isac/Interpret/ctree.sml") 

    11   ("~~/src/Tools/isac/Interpret/ptyps.sml") 

    12   ("~~/src/Tools/isac/Interpret/generate.sml")

    13   ("~~/src/Tools/isac/Interpret/calchead.sml") 

    14   ("~~/src/Tools/isac/Interpret/appl.sml") 

    15   ("~~/src/Tools/isac/Interpret/rewtools.sml") 

    16   ("~~/src/Tools/isac/Interpret/script.sml")

    17   ("~~/src/Tools/isac/Interpret/solve.sml") 

    18   ("~~/src/Tools/isac/Interpret/inform.sml") 

    19   ("~~/src/Tools/isac/Interpret/mathengine.sml")

    20 begin

    21   use "~~/src/Tools/isac/Interpret/mstools.sml"

    22   use "~~/src/Tools/isac/Interpret/ctree.sml"

    23   use "~~/src/Tools/isac/Interpret/ptyps.sml"

    24   use "~~/src/Tools/isac/Interpret/generate.sml"

    25   use "~~/src/Tools/isac/Interpret/calchead.sml"

    26   use "~~/src/Tools/isac/Interpret/appl.sml"

    27   use "~~/src/Tools/isac/Interpret/rewtools.sml"

    28   use "~~/src/Tools/isac/Interpret/script.sml"

    29   use "~~/src/Tools/isac/Interpret/solve.sml"

    30   use "~~/src/Tools/isac/Interpret/inform.sml"

    31   use "~~/src/Tools/isac/Interpret/mathengine.sml"

    32 end
wneuper/isa