1.1 --- a/src/Tools/isac/Build_Isac.thy	Wed Aug 28 07:08:25 2019 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Wed Aug 28 11:21:26 2019 +0200
     1.3 @@ -34,8 +34,8 @@
     1.4        ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"
     1.5    theory ProgLang imports Atools
     1.6  *)        "ProgLang/ProgLang"
     1.7 -
     1.8 -(*ML_file model.sml
     1.9 +(*
    1.10 +  ML_file model.sml
    1.11    ML_file mstools.sml
    1.12    ML_file "specification-elems.sml"
    1.13    ML_file istate.sml
    1.14 @@ -49,28 +49,27 @@
    1.15    ML_file calchead.sml
    1.16    ML_file appl.sml
    1.17  *)        "Specify/Specify"
    1.18 -
    1.19 -(*ML_file rewtools.sml
    1.20 +(*
    1.21 +  ML_file rewtools.sml
    1.22    ML_file script.sml
    1.23    ML_file inform.sml
    1.24    ML_file "lucas-interpreter.sml"
    1.25 +*)        "Interpret/Interpret"
    1.26 +(*
    1.27    ML_file solve.sml
    1.28    ML_file mathengine.sml
    1.29 -*)        "Interpret/Interpret"
    1.30 -
    1.31 -(*ML_file "~~/src/Tools/isac/xmlsrc/mathml.sml"
    1.32 -  ML_file "~~/src/Tools/isac/xmlsrc/datatypes.sml"
    1.33 -  ML_file "~~/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml"
    1.34 -  ML_file "~~/src/Tools/isac/xmlsrc/thy-hierarchy.sml" 
    1.35 -  ML_file "~~/src/Tools/isac/xmlsrc/interface-xml.sml"
    1.36 -*)        "xmlsrc/xmlsrc"
    1.37 -
    1.38 -(*ML_file "~~/src/Tools/isac/Frontend/messages.sml"
    1.39 -  ML_file "~~/src/Tools/isac/Frontend/states.sml"
    1.40 -  ML_file "~~/src/Tools/isac/Frontend/interface.sml"
    1.41 -
    1.42 -  ML_file "~~/src/Tools/isac/print_exn_G.sml"
    1.43 -*)         "Frontend/Frontend"
    1.44 +  ML_file "~~/src/Tools/isac/Frontend/messages.sml"
    1.45 +  ML_file messages.sml
    1.46 +  ML_file states.sml
    1.47 +*)        "MathEngine/MathEngine"
    1.48 +(*
    1.49 +  ML_file mathml.sml
    1.50 +  ML_file datatypes.sml
    1.51 +  ML_file "pbl-met-hierarchy.sml"
    1.52 +  ML_file "thy-hierarchy.sml" 
    1.53 +  ML_file "interface-xml.sml"
    1.54 +  ML_file interface.sml
    1.55 +*)        "BridgeLibisabelle/BridgeLibisabelle"
    1.56  
    1.57             "Knowledge/Build_Thydata" (*imports Isac.thy etc*)
    1.58  
    1.59 @@ -98,7 +97,6 @@
    1.60  ML \<open>Input_Descript.is_reall_dsc; (*from "ProgLang/scrtools.sml" *)\<close>
    1.61  ML \<open>Math_Engine.me; (*from "Interpret/mathengine.sml"*)\<close>
    1.62  ML \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close>
    1.63 -ML \<open>print_exn_unit\<close>
    1.64  ML \<open>list_rls (*from Atools.thy WN130615??? or ProgLang???*)\<close>
    1.65                                                           
    1.66  ML \<open>eval_occurs_in (*from Atools.thy*)\<close>