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

12345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80

*)

header {* Loading the isac mathengine *}

theory Build_Isac

imports Complex_Main

uses ("library.sml")

     ("calcelems.sml")

begin

  use "library.sml"

  use "calcelems.sml"

ML {*

@{term True}

*}

ML {*

@{term False}

*}

text {*

@{term True}

@{term False}

*}

(*

   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