(*  Title:   ~~~/isac/Isac_Mathengine.thy

    Author: Walther Neuper, TU Graz

$ cd /usr/local/Isabelle2009-1/src/Tools/isac

$ /usr/local/isabisac/bin/isabelle emacs Build_Isac.thy &

$ /usr/local/isabisac/bin/isabelle jedit Build_Isac.thy &

12345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80

*)

header {* Loading the isac mathengine *}

theory Build_Isac

(*imports Complex_Main*)

imports Complex_Main "ProgLang/Script" 

  (*ListC, Tools, Script*)

begin

ML {* 

writeln "**** build the isac kernel = math-engine + Knowledge ***********";

writeln "**** build the math-engine *************************************" *}

ML {* Toplevel.debug := true; *}

use "library.sml"

use "calcelems.sml"

ML {* check_guhs_unique := true *}

use "ProgLang/term.sml"

use "ProgLang/calculate.sml"

use "ProgLang/rewrite.sml"

use_thy"ProgLang/Script"

use "ProgLang/scrtools.sml"

use "Interpret/mstools.sml"

use "Interpret/ctree.sml"

use "Interpret/ptyps.sml"

use "Interpret/generate.sml"

use "Interpret/calchead.sml"

use "Interpret/appl.sml"

use "Interpret/rewtools.sml"

use "Interpret/script.sml"

use "Interpret/solve.sml"

use "Interpret/inform.sml"

use "Interpret/mathengine.sml"

use "xmlsrc/mathml.sml"

use "xmlsrc/datatypes.sml"

use "xmlsrc/pbl-met-hierarchy.sml"

use "xmlsrc/thy-hierarchy.sml" 

use "xmlsrc/interface-xml.sml"

use "Frontend/messages.sml"

use "Frontend/states.sml"

use "Frontend/interface.sml"

use "print_exn_G.sml"

ML {* writeln "**** build math-engine complete **************************" *}

ML {* writeln "**** build the Knowledge *********************************" *}

use_thy "Knowledge/Typefix"

use_thy "Knowledge/Descript"

ML {*

111;

*}

use_thy "Knowledge/Atools"

ML {*

val str = "1234567890";

*}

(*

use_thy "Knowledge/Simplify"

use_thy "Knowledge/Poly"

use_thy "Knowledge/Rational"

use_thy "Knowledge/PolyMinus"

use_thy "Knowledge/Equation"

use_thy "Knowledge/LinEq"

use_thy "Knowledge/Root"

use_thy "Knowledge/RootEq"

use_thy "Knowledge/RatEq"

use_thy "Knowledge/RootRat"

use_thy "Knowledge/RootRatEq"

use_thy "Knowledge/PolyEq"

use_thy "Knowledge/Vect"

use_thy "Knowledge/Calculus"

use_thy "Knowledge/Trig"

use_thy "Knowledge/LogExp"

use_thy "Knowledge/Diff"

use_thy "Knowledge/DiffApp"

use_thy "Knowledge/Integrate"

use_thy "Knowledge/EqSystem"

use_thy "Knowledge/Biegelinie"

use_thy "Knowledge/AlgEin"

use_thy "Knowledge/Test"

use_thy "Knowledge/Isac"

*)

end