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"