(*  Title:  build and test isac on Isabelle2013

    Author: Walther Neuper, TU Graz, 100808

   (c) due to copyright terms

For creating a heap image of isac see ~~/ROOT.

ATTENTION: no errors in this theory do not mean that there are no errors in Isac;

errors are rigorously detected when creating a heap.

*)

header {* Loading the isac mathengine;

  for debugging see text at begin (theory dependencies!) *}

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/Build_Thydata" (*imports Isac.thy etc*)

begin

text {* 

  show theory dependencies using the graph browser, 

  open "browser_info/HOL/Isac/session.graph"

  and proceed from the ancestors towards the siblings.

*}

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 WN130615??? or ProgLang???*) *}

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

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

ML {*@{thm Querkraft_Belastung}*}

ML {* check_guhs_unique := false; *}

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

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

ML {* ! isab_thm_thy *}

end