neuper@37906: (*  Title:   ~~~/isac/Isac_Mathengine.thy
neuper@37906:     Author: Walther Neuper, TU Graz
neuper@37906: 
neuper@37910: $ cd /usr/local/Isabelle2009-1/src/Tools/isac
neuper@37947: $ /usr/local/isabisac/bin/isabelle emacs Build_Isac.thy &
neuper@37947: $ /usr/local/isabisac/bin/isabelle jedit Build_Isac.thy &
neuper@37906: 
neuper@37924: 12345678901234567890123456789012345678901234567890123456789012345678901234567890
neuper@37924:         10        20        30        40        50        60        70        80
neuper@37906: *)
neuper@37906: 
neuper@37906: header {* Loading the isac mathengine *}
neuper@37906: 
neuper@37947: theory Build_Isac
neuper@38004: imports Complex_Main "ProgLang/Language" 
neuper@37906: begin
neuper@37906: 
neuper@37943: ML {* 
neuper@37947: writeln "**** build the isac kernel = math-engine + Knowledge ***********";
neuper@37947: writeln "**** build the math-engine *************************************" *}
neuper@37943: 
neuper@37906: ML {* Toplevel.debug := true; *}
neuper@37906: use "library.sml"
neuper@37906: use "calcelems.sml"
neuper@37906: ML {* check_guhs_unique := true *}
neuper@37906: 
neuper@37947: use "ProgLang/term.sml"
neuper@37947: use "ProgLang/calculate.sml"
neuper@37947: use "ProgLang/rewrite.sml"
neuper@37965: use_thy"ProgLang/Script" (*ListC, Tools, Script*)
neuper@37947: use "ProgLang/scrtools.sml"
neuper@37965: use_thy"ProgLang/Language"
neuper@37906: 
neuper@37947: use "Interpret/mstools.sml"
neuper@37947: use "Interpret/ctree.sml"
neuper@37947: use "Interpret/ptyps.sml"
neuper@37947: use "Interpret/generate.sml"
neuper@37947: use "Interpret/calchead.sml"
neuper@37947: use "Interpret/appl.sml"
neuper@37947: use "Interpret/rewtools.sml"
neuper@37947: use "Interpret/script.sml"
neuper@37947: use "Interpret/solve.sml"
neuper@37947: use "Interpret/inform.sml"
neuper@37947: use "Interpret/mathengine.sml"
neuper@37936: 
neuper@37940: use "xmlsrc/mathml.sml"
neuper@37940: use "xmlsrc/datatypes.sml"
neuper@37940: use "xmlsrc/pbl-met-hierarchy.sml"
neuper@37940: use "xmlsrc/thy-hierarchy.sml" 
neuper@37941: use "xmlsrc/interface-xml.sml"
neuper@37941: 
neuper@37947: use "Frontend/messages.sml"
neuper@37947: use "Frontend/states.sml"
neuper@37947: use "Frontend/interface.sml"
neuper@37906: 
neuper@37906: use "print_exn_G.sml"
neuper@37947: ML {* writeln "**** build math-engine complete **************************" *}
neuper@37906: 
neuper@37947: ML {* writeln "**** build the Knowledge *********************************" *}
neuper@38007: (*use_thy "Knowledge/Delete"
neuper@37979:   use_thy "Knowledge/Descript"
neuper@37979:   use_thy "Knowledge/Atools"
neuper@37979:   use_thy "Knowledge/Simplify"
neuper@37979:   use_thy "Knowledge/Poly"
neuper@38004:   use_thy "Knowledge/Rational"
neuper@38004:   use_thy "Knowledge/PolyMinus"
neuper@38004:   use_thy "Knowledge/Equation"
neuper@38004:   use_thy "Knowledge/LinEq"
neuper@38004:   use_thy "Knowledge/Root"
neuper@38004:   use_thy "Knowledge/RootEq"
neuper@38004:   use_thy "Knowledge/RatEq"
neuper@38004:   use_thy "Knowledge/RootRat"
neuper@38004:   use_thy "Knowledge/RootRatEq"
neuper@38004:   use_thy "Knowledge/PolyEq"
neuper@38004:   use_thy "Knowledge/Vect"
neuper@38004:   use_thy "Knowledge/Calculus"
neuper@38004:   use_thy "Knowledge/Trig"
neuper@38004:   use_thy "Knowledge/LogExp"
neuper@38004:   use_thy "Knowledge/Diff"
neuper@38004:   use_thy "Knowledge/DiffApp"
neuper@38004:   use_thy "Knowledge/Integrate"
neuper@38004:   use_thy "Knowledge/EqSystem"
neuper@38004:   use_thy "Knowledge/Biegelinie"
neuper@38004:   use_thy "Knowledge/AlgEin"
neuper@38007:   use_thy "Knowledge/Test"
neuper@38007: *)
neuper@38005: use_thy "Knowledge/Isac"
neuper@38005: 
neuper@37906: end
neuper@37906: