1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Build_Test_Isac.thy	Mon Sep 27 13:35:06 2010 +0200
     1.3 @@ -0,0 +1,100 @@
     1.4 +(*  Title:   ~~~/isac/Isac_Mathengine.thy
     1.5 +    Author: Walther Neuper, TU Graz
     1.6 +
     1.7 +$ cd /usr/local/Isabelle2009-1/src/Tools/isac
     1.8 +$ /usr/local/isabisac/bin/isabelle emacs Build_Isac.thy &
     1.9 +$ /usr/local/isabisac/bin/isabelle jedit Build_Isac.thy &
    1.10 +
    1.11 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
    1.12 +        10        20        30        40        50        60        70        80
    1.13 +*)
    1.14 +
    1.15 +header {* Loading the isac mathengine *}
    1.16 +
    1.17 +theory Build_Isac
    1.18 +imports Complex_Main "ProgLang/Language" (*"Knowledge/Test"*)
    1.19 +begin
    1.20 +
    1.21 +ML {* 
    1.22 +tracing "**** build the isac kernel = math-engine + Knowledge ***********";
    1.23 +tracing "**** build the math-engine *************************************" *}
    1.24 +
    1.25 +ML {* Toplevel.debug := true; *}
    1.26 +use "library.sml"
    1.27 +use "calcelems.sml"
    1.28 +ML {* check_guhs_unique := true *}
    1.29 +
    1.30 +use "ProgLang/term.sml"
    1.31 +use "ProgLang/calculate.sml"
    1.32 +use "ProgLang/rewrite.sml"
    1.33 +use_thy"ProgLang/Script"    (*ListC, Tools, Script*)
    1.34 +use "ProgLang/scrtools.sml"
    1.35 +use_thy"ProgLang/Language"  (*just for integrating scrtools.sml*)
    1.36 +
    1.37 +use "Interpret/mstools.sml"
    1.38 +use "Interpret/ctree.sml"
    1.39 +use "Interpret/ptyps.sml"
    1.40 +use "Interpret/generate.sml"
    1.41 +use "Interpret/calchead.sml"
    1.42 +use "Interpret/appl.sml"
    1.43 +use "Interpret/rewtools.sml"
    1.44 +use "Interpret/script.sml"
    1.45 +use "Interpret/solve.sml"
    1.46 +use "Interpret/inform.sml"
    1.47 +use "Interpret/mathengine.sml"
    1.48 +
    1.49 +use "xmlsrc/mathml.sml"
    1.50 +use "xmlsrc/datatypes.sml"
    1.51 +use "xmlsrc/pbl-met-hierarchy.sml"
    1.52 +use "xmlsrc/thy-hierarchy.sml" 
    1.53 +use "xmlsrc/interface-xml.sml"
    1.54 +
    1.55 +use "Frontend/messages.sml"
    1.56 +use "Frontend/states.sml"
    1.57 +use "Frontend/interface.sml"
    1.58 +
    1.59 +use "print_exn_G.sml"
    1.60 +ML {* tracing "**** build math-engine complete **************************" *}
    1.61 +
    1.62 +ML {* tracing "**** build the Knowledge *********************************" *}
    1.63 +(*use_thy "Knowledge/Delete"
    1.64 +  use_thy "Knowledge/Descript"
    1.65 +  use_thy "Knowledge/Atools"
    1.66 +  use_thy "Knowledge/Simplify"
    1.67 +  use_thy "Knowledge/Poly"
    1.68 +  use_thy "Knowledge/Rational"
    1.69 +  use_thy "Knowledge/PolyMinus"
    1.70 +  use_thy "Knowledge/Equation"
    1.71 +  use_thy "Knowledge/LinEq"
    1.72 +  use_thy "Knowledge/Root"
    1.73 +  use_thy "Knowledge/RootEq"
    1.74 +  use_thy "Knowledge/RatEq"
    1.75 +  use_thy "Knowledge/RootRat"
    1.76 +  use_thy "Knowledge/RootRatEq"
    1.77 +  use_thy "Knowledge/PolyEq"
    1.78 +  use_thy "Knowledge/Vect"
    1.79 +  use_thy "Knowledge/Calculus"
    1.80 +  use_thy "Knowledge/Trig"
    1.81 +  use_thy "Knowledge/LogExp"
    1.82 +  use_thy "Knowledge/Diff"
    1.83 +  use_thy "Knowledge/DiffApp"
    1.84 +  use_thy "Knowledge/Integrate"
    1.85 +  use_thy "Knowledge/EqSystem"
    1.86 +  use_thy "Knowledge/Biegelinie"
    1.87 +  use_thy "Knowledge/AlgEin"
    1.88 +*)
    1.89 +use_thy "Knowledge/Test" (*required _only_ for ROOT.ML !?!*)
    1.90 +use_thy "Knowledge/Isac"
    1.91 +ML {* check_guhs_unique := false; *}
    1.92 +ML {* tracing "**** isac kernel = math-engine + Knowledge complete ******" *}
    1.93 +
    1.94 +(*
    1.95 +use "../../../test/Tools/isac/Interpret/calchead.sml" (*part.*)
    1.96 +*** get_pbt not found: ["linear","system"]
    1.97 +use"../../../test/Tools/isac/Knowledge/integrate.sml";
    1.98 +*)
    1.99 +ML{* writeln "**** run the tests **************************************" *};
   1.100 +use_thy "Test_Isac"
   1.101 +
   1.102 +end
   1.103 +