equal
deleted
inserted
replaced
10 *) |
10 *) |
11 |
11 |
12 header {* Loading the isac mathengine *} |
12 header {* Loading the isac mathengine *} |
13 |
13 |
14 theory Build_Isac |
14 theory Build_Isac |
15 imports Complex_Main "ProgLang/Language" |
15 imports Complex_Main "ProgLang/Language" (*"Knowledge/Test"*) |
16 begin |
16 begin |
17 |
17 |
18 ML {* |
18 ML {* |
19 writeln "**** build the isac kernel = math-engine + Knowledge ***********"; |
19 writeln "**** build the isac kernel = math-engine + Knowledge ***********"; |
20 writeln "**** build the math-engine *************************************" *} |
20 writeln "**** build the math-engine *************************************" *} |
25 ML {* check_guhs_unique := true *} |
25 ML {* check_guhs_unique := true *} |
26 |
26 |
27 use "ProgLang/term.sml" |
27 use "ProgLang/term.sml" |
28 use "ProgLang/calculate.sml" |
28 use "ProgLang/calculate.sml" |
29 use "ProgLang/rewrite.sml" |
29 use "ProgLang/rewrite.sml" |
30 use_thy"ProgLang/Script" (*ListC, Tools, Script*) |
30 use_thy"ProgLang/Script" (*ListC, Tools, Script*) |
31 use "ProgLang/scrtools.sml" |
31 use "ProgLang/scrtools.sml" |
32 use_thy"ProgLang/Language" |
32 use_thy"ProgLang/Language" (*just for integrating scrtools.sml*) |
33 |
33 |
34 use "Interpret/mstools.sml" |
34 use "Interpret/mstools.sml" |
35 use "Interpret/ctree.sml" |
35 use "Interpret/ctree.sml" |
36 use "Interpret/ptyps.sml" |
36 use "Interpret/ptyps.sml" |
37 use "Interpret/generate.sml" |
37 use "Interpret/generate.sml" |
83 use_thy "Knowledge/Biegelinie" |
83 use_thy "Knowledge/Biegelinie" |
84 use_thy "Knowledge/AlgEin" |
84 use_thy "Knowledge/AlgEin" |
85 use_thy "Knowledge/Test" |
85 use_thy "Knowledge/Test" |
86 *) |
86 *) |
87 use_thy "Knowledge/Isac" |
87 use_thy "Knowledge/Isac" |
|
88 check_guhs_unique := false; |
|
89 ML {* writeln "**** isac kernel = math-engine + Knowledge complete ******" *} |
88 |
90 |
89 end |
91 end |
90 |
92 |