equal
deleted
inserted
replaced
1 (* Title: ~~~/isac/Isac_Mathengine.thy |
1 (* Title: ~~~/isac/Isac_Mathengine.thy |
2 Author: Walther Neuper, TU Graz |
2 Author: Walther Neuper, TU Graz |
3 |
3 |
4 $ cd /usr/local/Isabelle2009-1/src/Tools/isac |
4 $ cd /usr/local/Isabelle2009-1/src/Tools/isac |
5 $ /usr/local/isabisac/bin/isabelle emacs Build_Isac.thy & |
5 $ /usr/local/isabisac/bin/isabelle emacs Build_Test_Isac.thy & |
6 $ /usr/local/isabisac/bin/isabelle jedit Build_Isac.thy & |
6 $ /usr/local/isabisac/bin/isabelle jedit Build_Test_Isac.thy & |
7 |
7 |
8 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
8 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
9 10 20 30 40 50 60 70 80 |
9 10 20 30 40 50 60 70 80 |
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_Test_Isac |
15 imports Complex_Main "ProgLang/Language" (*"Knowledge/Test"*) |
15 imports Complex_Main "ProgLang/Language" (*"Knowledge/Test"*) |
16 begin |
16 begin |
17 |
17 |
18 ML {* |
18 ML {* |
19 tracing "**** build the isac kernel = math-engine + Knowledge ***********"; |
19 tracing "**** build the isac kernel = math-engine + Knowledge ***********"; |