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/Frontend/Frontend.thy
author Walther Neuper <wneuper@ist.tugraz.at>
Tue, 18 Oct 2016 12:05:03 +0200
changeset 59252 7d3dbc1171ff
parent 59138 edb5ce92451e
child 59472 3e904f8ec16c
permissions -rw-r--r--
back-track after desing error in previous changeset

notes (the latter of 2 desastrous changesets):
# error was: in Isac thm must be accompanied with thmID,
because Thm.get_name_hint reports "unknown" after ".. RS sym"
# improved design will be: Rewrite* and Rewrite'* take arg. (thmID, thm)
# previous changeset also destroyed "fun pbl2xml" 
     1 (* Title:  collect all defitions for the Frontend

     2    Author: Walther Neuper 110226

     3    (c) due to copyright terms

     4  *)

     5 

     6 theory Frontend 

     7 imports "~~/src/Tools/isac/xmlsrc/xmlsrc"

     8 begin

     9 

    10   ML_file "~~/src/Tools/isac/Frontend/messages.sml"

    11   ML_file "~~/src/Tools/isac/Frontend/states.sml"

    12   ML_file "~~/src/Tools/isac/Frontend/interface.sml"

    13 

    14   ML_file "~~/src/Tools/isac/print_exn_G.sml"

    15 

    16 ML {*

    17 *} ML {*

    18 *} 

    19 end
wneuper/isa