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/xmlsrc/xmlsrc.thy
author Walther Neuper <wneuper@ist.tugraz.at>
Thu, 22 Dec 2016 10:25:49 +0100
changeset 59276 56dc790071cb
parent 59250 727dff4f6b2c
child 59341 e366a514a46e
permissions -rw-r--r--
--- closed structure Ctree

Notes:
# "closed" means removed "open Ctree" immediately after respective end.
# test do not work (with "! activate for Test_Isac") due to 1 "open Ctree,
see next changeset. 
     1 (* Title:  collect all defitions for xml generation

     2    Author: Walther Neuper 110226

     3    (c) due to copyright terms

     4 *)

     5 

     6 theory xmlsrc 

     7 imports "~~/libisabelle-protocol/protocol/Codec_Class" "~~/src/Tools/isac/Interpret/Interpret"

     8 

     9 begin

    10 

    11   ML_file "~~/src/Tools/isac/xmlsrc/mathml.sml"

    12   ML_file "~~/src/Tools/isac/xmlsrc/datatypes.sml"

    13   ML_file "~~/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml"

    14   ML_file "~~/src/Tools/isac/xmlsrc/thy-hierarchy.sml" 

    15   ML_file "~~/src/Tools/isac/xmlsrc/interface-xml.sml"

    16 (*declare [[ML_print_depth = 999]]*)

    17 ML {*

    18 *} ML {*

    19 *}

    20 

    21 end
wneuper/isa