src/Tools/isac/Knowledge/Atools.thy
branchisac-update-Isa09-2
changeset 38011 3147f2c1525c
parent 37999 7d603b7ead73
child 38014 3e11e3c2dc42
     1.1 --- a/src/Tools/isac/Knowledge/Atools.thy	Tue Sep 14 15:46:56 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Atools.thy	Thu Sep 23 08:43:36 2010 +0200
     1.3 @@ -13,25 +13,33 @@
     1.4  ("Interpret/inform.sml")("Interpret/mathengine.sml")
     1.5  ("xmlsrc/mathml.sml")("xmlsrc/datatypes.sml")("xmlsrc/pbl-met-hierarchy.sml")
     1.6  ("xmlsrc/thy-hierarchy.sml")("xmlsrc/interface-xml.sml")
     1.7 +("Frontend/messages.sml")("Frontend/states.sml")("Frontend/interface.sml")
     1.8 +("print_exn_G.sml")
     1.9  begin
    1.10  use "Interpret/mstools.sml"
    1.11  use "Interpret/ctree.sml"
    1.12 -use "Interpret/ptyps.sml"   (*^^^ need files for: fun prep_pbt, fun store_pbt*)
    1.13 +use "Interpret/ptyps.sml"    (*^^^ need files for: fun prep_pbt, fun store_pbt*)
    1.14  use "Interpret/generate.sml"
    1.15  use "Interpret/calchead.sml"
    1.16  use "Interpret/appl.sml"
    1.17  use "Interpret/rewtools.sml"
    1.18  use "Interpret/script.sml"
    1.19  use "Interpret/solve.sml"
    1.20 -use "Interpret/inform.sml"  (*^^^ need files for: fun castab*)
    1.21 +use "Interpret/inform.sml"       (*^^^ need files for: fun castab*)
    1.22  use "Interpret/mathengine.sml"
    1.23  
    1.24  use "xmlsrc/mathml.sml"
    1.25  use "xmlsrc/datatypes.sml"
    1.26  use "xmlsrc/pbl-met-hierarchy.sml"
    1.27 -use "xmlsrc/thy-hierarchy.sml" (*^^^ need files for: fun store_isa*)
    1.28 +use "xmlsrc/thy-hierarchy.sml"   (*^^^ need files for: fun store_isa*)
    1.29  use "xmlsrc/interface-xml.sml"
    1.30  
    1.31 +use "Frontend/messages.sml"
    1.32 +use "Frontend/states.sml"    (*^^^ need files for: val states in Test_Isac.thy*)
    1.33 +use "Frontend/interface.sml"
    1.34 +
    1.35 +use "print_exn_G.sml"
    1.36 +
    1.37  consts
    1.38  
    1.39    Arbfix           :: "real"