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