neuper@38070: (*  Title:  build and test isac 
neuper@38057:     Author: Walther Neuper, TU Graz, 100808
neuper@38051:    (c) due to copyright terms
neuper@38051: 
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@38057: create a new Isac heap (via ~~/ROOT.ML) with
neuper@38057: $ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac
neuper@38057: 
neuper@38063: start with Isac
neuper@38063: $ /usr/local/isabisac/bin/isabelle emacs -l Isac Build_Isac.thy &
neuper@38063: $ /usr/local/isabisac/bin/isabelle jedit -l Isac Build_Isac.thy &
neuper@38063: 
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@41905: theory Build_Isac imports Complex_Main
neuper@41905: (* use    "library.sml"
neuper@41905:    use    "calcelems.sml"
neuper@41905: 
neuper@41905:    use    "ProgLang/termC.sml"
neuper@41905:    use    "ProgLang/calculate.sml"
neuper@41905:    use    "ProgLang/rewrite.sml"
neuper@41905:   "use_thy ProgLang/ListC"
neuper@41905:   "use_thy ProgLang/Tools"
neuper@41905:   "use_thy ProgLang/Script"
neuper@41905:    use    "ProgLang/scrtools.sml"
neuper@41905: *)        "ProgLang/Language"
neuper@41905: 
neuper@41905: (* use    "Interpret/mstools.sml"
neuper@41905:    use    "Interpret/ctree.sml"
neuper@41905:    use    "Interpret/ptyps.sml"
neuper@41905:    use    "Interpret/generate.sml"
neuper@41905:    use    "Interpret/calchead.sml"
neuper@41905:    use    "Interpret/appl.sml"
neuper@41905:    use    "Interpret/rewtools.sml"
neuper@41905:    use    "Interpret/script.sml"
neuper@41905:    use    "Interpret/solve.sml"
neuper@41905:    use    "Interpret/inform.sml"
neuper@41905:    use    "Interpret/mathengine.sml"
neuper@41905: *)        "Interpret/Interpret"
neuper@41905: 
neuper@41905: (* use    "xmlsrc/mathml.sml"
neuper@41905:    use    "xmlsrc/datatypes.sml"
neuper@41905:    use    "xmlsrc/pbl-met-hierarchy.sml"
neuper@41905:    use    "xmlsrc/thy-hierarchy.sml" 
neuper@41905:    use    "xmlsrc/interface-xml.sml"
neuper@41905: *)        "xmlsrc/xmlsrc"
neuper@41905: 
neuper@41905: (* use     "Frontend/messages.sml"
neuper@41905:    use     "Frontend/states.sml"
neuper@41905:    use     "Frontend/interface.sml"
neuper@41905: 
neuper@41905:    use     "print_exn_G.sml"
neuper@41905: *)         "Frontend/Frontend"
neuper@37906: begin
neuper@41905: ML {* is_reall_dsc; (*from "ProgLang/scrtools.sml" *) *}
neuper@41905: ML {* me; (*from "Interpret/mathengine.sml"*) *}
neuper@41905: ML {* contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*) *}
neuper@41905: ML {* print_exn_unit *}
neuper@41905: ML {*1*}
neuper@37906: 
neuper@38015: ML {* tracing "**** build the Knowledge *********************************" *}
neuper@41905: (**)
neuper@41905: use_thy "Knowledge/Delete"
neuper@37979:   use_thy "Knowledge/Descript"
neuper@37979:   use_thy "Knowledge/Atools"
neuper@41905: ML {* list_rls (*from Atools.thy*) *}
neuper@41905: ML {* eval_occurs_in (*from Atools.thy*) *}
neuper@41905: ML {* @{thm last_thmI} (*from Atools.thy*) *}
neuper@41905: 
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@41905: 
neuper@41905: ML {*
neuper@41905: @{thm Querkraft_Belastung}
neuper@41905: *}
neuper@41905: 
neuper@38010:   use_thy "Knowledge/Test" (*required _only_ for ROOT.ML !?!*)
neuper@38005: use_thy "Knowledge/Isac"
neuper@38057: 
neuper@38009: ML {* check_guhs_unique := false; *}
neuper@38015: ML {* tracing "**** isac kernel = math-engine + Knowledge complete ******" *}
neuper@38005: 
neuper@37906: end
neuper@37906: 
neuper@38057: (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
neuper@38057: -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)