tuned isac-update-Isa09-2
authorWalther Neuper <neuper@ist.tugraz.at>
Mon, 13 Sep 2010 18:37:16 +0200
branchisac-update-Isa09-2
changeset 3800879b6cbd02681
parent 38007 d679c1f837a7
child 38009 b49723351533
tuned
src/Tools/isac/Build_Isac.thy
     1.1 --- a/src/Tools/isac/Build_Isac.thy	Mon Sep 13 18:12:15 2010 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Mon Sep 13 18:37:16 2010 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  header {* Loading the isac mathengine *}
     1.5  
     1.6  theory Build_Isac
     1.7 -imports Complex_Main "ProgLang/Language" 
     1.8 +imports Complex_Main "ProgLang/Language" (*"Knowledge/Test"*)
     1.9  begin
    1.10  
    1.11  ML {* 
    1.12 @@ -27,9 +27,9 @@
    1.13  use "ProgLang/term.sml"
    1.14  use "ProgLang/calculate.sml"
    1.15  use "ProgLang/rewrite.sml"
    1.16 -use_thy"ProgLang/Script" (*ListC, Tools, Script*)
    1.17 +use_thy"ProgLang/Script"    (*ListC, Tools, Script*)
    1.18  use "ProgLang/scrtools.sml"
    1.19 -use_thy"ProgLang/Language"
    1.20 +use_thy"ProgLang/Language"  (*just for integrating scrtools.sml*)
    1.21  
    1.22  use "Interpret/mstools.sml"
    1.23  use "Interpret/ctree.sml"
    1.24 @@ -85,6 +85,8 @@
    1.25    use_thy "Knowledge/Test"
    1.26  *)
    1.27  use_thy "Knowledge/Isac"
    1.28 +check_guhs_unique := false;
    1.29 +ML {* writeln "**** isac kernel = math-engine + Knowledge complete ******" *}
    1.30  
    1.31  end
    1.32