1 (* Title: ~~~/isac/Isac_Mathengine.thy |
1 (* Title: build and test isac |
2 Author: Walther Neuper, TU Graz |
2 Author: Walther Neuper, TU Graz, 100808 |
3 (c) due to copyright terms |
3 (c) due to copyright terms |
4 |
|
5 Code copied from respective parte of Build_Test_Isac.thy |
|
6 |
4 |
7 $ cd /usr/local/Isabelle2009-1/src/Tools/isac |
5 $ cd /usr/local/Isabelle2009-1/src/Tools/isac |
8 $ /usr/local/isabisac/bin/isabelle emacs Build_Isac.thy & |
6 $ /usr/local/isabisac/bin/isabelle emacs Build_Isac.thy & |
9 $ /usr/local/isabisac/bin/isabelle jedit Build_Isac.thy & |
7 $ /usr/local/isabisac/bin/isabelle jedit Build_Isac.thy & |
|
8 |
|
9 create a new Isac heap (via ~~/ROOT.ML) with |
|
10 $ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac |
10 |
11 |
11 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
12 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
12 10 20 30 40 50 60 70 80 |
13 10 20 30 40 50 60 70 80 |
13 *) |
14 *) |
14 |
15 |
15 header {* Loading the isac mathengine *} |
16 header {* Loading the isac mathengine *} |
16 |
17 |
17 theory Build_Isac |
18 theory Build_Isac |
18 imports Complex_Main "ProgLang/Language" (*"Knowledge/Test"*) |
19 imports Complex_Main "ProgLang/Language" (*"Knowledge/Isac"*) |
19 begin |
20 begin |
20 |
21 |
21 ML {* |
22 ML {* |
22 tracing "**** build the isac kernel = math-engine + Knowledge ***********"; |
23 tracing "**** build the isac kernel = math-engine + Knowledge ***********"; |
23 tracing "**** build the math-engine *************************************" *} |
24 tracing "**** build the math-engine *************************************" *} |
86 use_thy "Knowledge/Biegelinie" |
87 use_thy "Knowledge/Biegelinie" |
87 use_thy "Knowledge/AlgEin" |
88 use_thy "Knowledge/AlgEin" |
88 *) |
89 *) |
89 use_thy "Knowledge/Test" (*required _only_ for ROOT.ML !?!*) |
90 use_thy "Knowledge/Test" (*required _only_ for ROOT.ML !?!*) |
90 use_thy "Knowledge/Isac" |
91 use_thy "Knowledge/Isac" |
|
92 |
91 ML {* check_guhs_unique := false; *} |
93 ML {* check_guhs_unique := false; *} |
92 ML {* tracing "**** isac kernel = math-engine + Knowledge complete ******" *} |
94 ML {* tracing "**** isac kernel = math-engine + Knowledge complete ******" *} |
93 |
95 |
94 |
|
95 (* |
|
96 use "../../../test/Tools/isac/Interpret/calchead.sml" (*part.*) |
|
97 *** get_pbt not found: ["linear","system"] |
|
98 use"../../../test/Tools/isac/Knowledge/integrate.sml"; |
|
99 *) |
|
100 |
|
101 end |
96 end |
102 |
97 |
|
98 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
|
99 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) |