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