1 (* Title: ~~~/isac/Isac_Mathengine.thy |
|
2 Author: Walther Neuper, TU Graz |
|
3 |
|
4 $ cd /usr/local/Isabelle2009-1/src/Tools/isac |
|
5 $ /usr/local/isabisac/bin/isabelle emacs Isac_Mathengine.thy & |
|
6 $ /usr/local/isabisac/bin/isabelle jedit Isac_Mathengine.thy & |
|
7 |
|
8 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
|
9 10 20 30 40 50 60 70 80 |
|
10 *) |
|
11 |
|
12 header {* Loading the isac mathengine *} |
|
13 |
|
14 theory Isac_Mathengine |
|
15 (*imports Complex_Main*) |
|
16 imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*) |
|
17 begin |
|
18 |
|
19 ML {* |
|
20 writeln "**** build the isac kernel = math-engine + IsacKnowledge "; |
|
21 writeln "**** build the math-engine ******************************" *} |
|
22 |
|
23 ML {* Toplevel.debug := true; *} |
|
24 use "library.sml" |
|
25 use "calcelems.sml" |
|
26 ML {* check_guhs_unique := true *} |
|
27 |
|
28 use "Scripts/term_G.sml" |
|
29 use "Scripts/calculate.sml" |
|
30 use "Scripts/rewrite.sml" |
|
31 use_thy"Scripts/Script" |
|
32 use "Scripts/scrtools.sml" |
|
33 |
|
34 use "ME/mstools.sml" |
|
35 use "ME/ctree.sml" |
|
36 use "ME/ptyps.sml" |
|
37 use "ME/generate.sml" |
|
38 use "ME/calchead.sml" |
|
39 use "ME/appl.sml" |
|
40 use "ME/rewtools.sml" |
|
41 use "ME/script.sml" |
|
42 use "ME/solve.sml" |
|
43 use "ME/inform.sml" |
|
44 use "ME/mathengine.sml" |
|
45 |
|
46 use "xmlsrc/mathml.sml" |
|
47 use "xmlsrc/datatypes.sml" |
|
48 use "xmlsrc/pbl-met-hierarchy.sml" |
|
49 use "xmlsrc/thy-hierarchy.sml" |
|
50 use "xmlsrc/interface-xml.sml" |
|
51 |
|
52 use "FE-interface/messages.sml" |
|
53 use "FE-interface/states.sml" |
|
54 use "FE-interface/interface.sml" |
|
55 |
|
56 use "print_exn_G.sml" |
|
57 text "**** build math-engine complete *************************" |
|
58 |
|
59 ML {* writeln "**** build the IsacKnowledge ****************************" *} |
|
60 use_thy"IsacKnowledge/Typefix" |
|
61 use_thy"IsacKnowledge/Descript" |
|
62 |
|
63 ML {* |
|
64 |
|
65 111; |
|
66 *} |
|
67 |
|
68 use_thy"IsacKnowledge/Atools" |
|
69 |
|
70 |
|
71 ML {* |
|
72 val str = "1234567890"; |
|
73 *} |
|
74 |
|
75 (* |
|
76 use_thy"IsacKnowledge/Simplify" |
|
77 use_thy"IsacKnowledge/Poly" |
|
78 use_thy"IsacKnowledge/Rational" |
|
79 use_thy"IsacKnowledge/PolyMinus" |
|
80 use_thy"IsacKnowledge/Equation" |
|
81 use_thy"IsacKnowledge/LinEq" |
|
82 use_thy"IsacKnowledge/Root" |
|
83 use_thy"IsacKnowledge/RootEq" |
|
84 use_thy"IsacKnowledge/RatEq" |
|
85 use_thy"IsacKnowledge/RootRat" |
|
86 use_thy"IsacKnowledge/RootRatEq" |
|
87 use_thy"IsacKnowledge/PolyEq" |
|
88 use_thy"IsacKnowledge/Vect" |
|
89 use_thy"IsacKnowledge/Calculus" |
|
90 use_thy"IsacKnowledge/Trig" |
|
91 use_thy"IsacKnowledge/LogExp" |
|
92 use_thy"IsacKnowledge/Diff" |
|
93 use_thy"IsacKnowledge/DiffApp" |
|
94 use_thy"IsacKnowledge/Integrate" |
|
95 use_thy"IsacKnowledge/EqSystem" |
|
96 use_thy"IsacKnowledge/Biegelinie" |
|
97 use_thy"IsacKnowledge/AlgEin" |
|
98 use_thy"IsacKnowledge/Test" |
|
99 use_thy"IsacKnowledge/Isac" |
|
100 *) |
|
101 end |
|
102 |
|