(*  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 "ProgLang/Language" 

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" (*ListC, Tools, Script*)

use "ProgLang/scrtools.sml"

use_thy"ProgLang/Language"

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/Delete"

  use_thy "Knowledge/Descript"

  use_thy "Knowledge/Atools"

  use_thy "Knowledge/Simplify"

  use_thy "Knowledge/Poly"

ML {*

val m = (1,[2]);

#1 m;

fst m;

*}

  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"

ML {* 111;

*}

use_thy "Knowledge/Isac"

text {*------------------------------------------*}

(*

*)

end