1.1 --- a/src/Tools/isac/Knowledge/Atools.thy	Sat Feb 26 12:53:00 2011 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Atools.thy	Tue Mar 01 15:23:59 2011 +0100
     1.3 @@ -6,40 +6,45 @@
     1.4          10        20        30        40        50        60        70        80
     1.5  *)
     1.6  
     1.7 -theory Atools imports Descript 
     1.8 -uses ("Interpret/mstools.sml")("Interpret/ctree.sml")("Interpret/ptyps.sml")
     1.9 -("Interpret/generate.sml")("Interpret/calchead.sml")("Interpret/appl.sml")
    1.10 -("Interpret/rewtools.sml")("Interpret/script.sml")("Interpret/solve.sml")
    1.11 -("Interpret/inform.sml")("Interpret/mathengine.sml")
    1.12 -("xmlsrc/mathml.sml")("xmlsrc/datatypes.sml")("xmlsrc/pbl-met-hierarchy.sml")
    1.13 -("xmlsrc/thy-hierarchy.sml")("xmlsrc/interface-xml.sml")
    1.14 -("Frontend/messages.sml")("Frontend/states.sml")("Frontend/interface.sml")
    1.15 -("print_exn_G.sml")
    1.16 +theory Atools imports Descript "../Interpret/Interpret"
    1.17 +(*
    1.18 +uses ("../Interpret/mstools.sml")("../Interpret/ctree.sml")
    1.19 +("../Interpret/ptyps.sml")("../Interpret/generate.sml")
    1.20 +("../Interpret/calchead.sml")("../Interpret/appl.sml")
    1.21 +("../Interpret/rewtools.sml")("../Interpret/script.sml")
    1.22 +("../Interpret/solve.sml")("../Interpret/inform.sml")
    1.23 +("../Interpret/mathengine.sml")("../xmlsrc/mathml.sml")
    1.24 +("../xmlsrc/datatypes.sml")("../xmlsrc/pbl-met-hierarchy.sml")
    1.25 +("../xmlsrc/thy-hierarchy.sml")("../xmlsrc/interface-xml.sml")
    1.26 +("../Frontend/messages.sml")("../Frontend/states.sml")
    1.27 +("../Frontend/interface.sml")("../print_exn_G.sml")
    1.28 +*)
    1.29  begin
    1.30 -use "Interpret/mstools.sml"
    1.31 -use "Interpret/ctree.sml"
    1.32 -use "Interpret/ptyps.sml"    (*^^^ need files for: fun prep_pbt, fun store_pbt*)
    1.33 -use "Interpret/generate.sml"
    1.34 -use "Interpret/calchead.sml"
    1.35 -use "Interpret/appl.sml"
    1.36 -use "Interpret/rewtools.sml"
    1.37 -use "Interpret/script.sml"
    1.38 -use "Interpret/solve.sml"
    1.39 -use "Interpret/inform.sml"       (*^^^ need files for: fun castab*)
    1.40 -use "Interpret/mathengine.sml"
    1.41 +(*
    1.42 +use "../Interpret/mstools.sml"
    1.43 +use "../Interpret/ctree.sml"
    1.44 +use "../Interpret/ptyps.sml"       (*^^^ need for: fun prep_pbt, fun store_pbt*)
    1.45 +use "../Interpret/generate.sml"
    1.46 +use "../Interpret/calchead.sml"
    1.47 +use "../Interpret/appl.sml"
    1.48 +use "../Interpret/rewtools.sml"
    1.49 +use "../Interpret/script.sml"
    1.50 +use "../Interpret/solve.sml"
    1.51 +use "../Interpret/inform.sml"                 (*^^^ need files for: fun castab*)
    1.52 +use "../Interpret/mathengine.sml"
    1.53  
    1.54 -use "xmlsrc/mathml.sml"
    1.55 -use "xmlsrc/datatypes.sml"
    1.56 -use "xmlsrc/pbl-met-hierarchy.sml"
    1.57 -use "xmlsrc/thy-hierarchy.sml"   (*^^^ need files for: fun store_isa*)
    1.58 -use "xmlsrc/interface-xml.sml"
    1.59 +use "../xmlsrc/mathml.sml"
    1.60 +use "../xmlsrc/datatypes.sml"
    1.61 +use "../xmlsrc/pbl-met-hierarchy.sml"
    1.62 +use "../xmlsrc/thy-hierarchy.sml"          (*^^^ need files for: fun store_isa*)
    1.63 +use "../xmlsrc/interface-xml.sml"
    1.64  
    1.65 -use "Frontend/messages.sml"
    1.66 -use "Frontend/states.sml"    (*^^^ need files for: val states in Test_Isac.thy*)
    1.67 -use "Frontend/interface.sml"
    1.68 +use "../Frontend/messages.sml"
    1.69 +use "../Frontend/states.sml"       (*^^^ need for: val states in Test_Isac.thy*)
    1.70 +use "../Frontend/interface.sml"
    1.71  
    1.72 -use "print_exn_G.sml"
    1.73 -
    1.74 +use "../print_exn_G.sml"
    1.75 +*)
    1.76  consts
    1.77  
    1.78    Arbfix           :: "real"