(*  Title:  build and test isac 

    Author: Walther Neuper, TU Graz, 100808

   (c) due to copyright terms

create a new Isac heap (via ~~/ROOT.ML) with

$ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac

start with heap Isac

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

12345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80

*)

header {* Loading the isac mathengine *}

theory Build_Isac imports Complex_Main

(* use    "library.sml"

   use    "calcelems.sml"

   use    "ProgLang/termC.sml"

   use    "ProgLang/calculate.sml"

   use    "ProgLang/rewrite.sml"

  "use_thy ProgLang/ListC"

  "use_thy ProgLang/Tools"

  "use_thy ProgLang/Script"

   use    "ProgLang/scrtools.sml"

*)        "ProgLang/ProgLang"

(* 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"

*)        "Interpret/Interpret"

(* use    "xmlsrc/mathml.sml"

   use    "xmlsrc/datatypes.sml"

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

   use    "xmlsrc/thy-hierarchy.sml" 

   use    "xmlsrc/interface-xml.sml"

*)        "xmlsrc/xmlsrc"

(* use     "Frontend/messages.sml"

   use     "Frontend/states.sml"

   use     "Frontend/interface.sml"

   use     "print_exn_G.sml"

*)         "Frontend/Frontend"

(*         "Knowledge/Isac"

*)

           "Knowledge/Build_Thydata"

begin

text {*check presence of definitions from directories*}

ML {* is_reall_dsc; (*from "ProgLang/scrtools.sml" *) *}

ML {* me; (*from "Interpret/mathengine.sml"*) *}

ML {* contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*) *}

ML {* print_exn_unit *}

ML {* list_rls (*from Atools.thy*) *}

ML {* eval_occurs_in (*from Atools.thy*) *}

ML {* @{thm last_thmI} (*from Atools.thy*) *}

ML {*@{thm Querkraft_Belastung}*}

ML {* check_guhs_unique := false; *}

ML {* tracing "**** isac kernel = math-engine + Knowledge complete ******" *}

ML {* @{theory "Isac"} *}

ML {* ! isab_thm_thy *}

end