1 (* Title: ~~~/isac/Isac_Mathengine.thy
2 Author: Walther Neuper, TU Graz
4 $ cd /usr/local/Isabelle2009-1/src/Tools/isac
5 $ /usr/local/isabisac/bin/isabelle emacs Build_Isac.thy &
6 $ /usr/local/isabisac/bin/isabelle jedit Build_Isac.thy &
8 12345678901234567890123456789012345678901234567890123456789012345678901234567890
9 10 20 30 40 50 60 70 80
12 header {* Loading the isac mathengine *}
15 imports Complex_Main "ProgLang/Script" (*ListC, Tools, Script*)
19 writeln "**** build the isac kernel = math-engine + Knowledge ***********";
20 writeln "**** build the math-engine *************************************" *}
22 ML {* Toplevel.debug := true; *}
25 ML {* check_guhs_unique := true *}
27 use "ProgLang/term.sml"
28 use "ProgLang/calculate.sml"
29 use "ProgLang/rewrite.sml"
30 use_thy"ProgLang/Script"
31 use "ProgLang/scrtools.sml"
33 use "Interpret/mstools.sml"
34 use "Interpret/ctree.sml"
35 use "Interpret/ptyps.sml"
36 use "Interpret/generate.sml"
37 use "Interpret/calchead.sml"
38 use "Interpret/appl.sml"
39 use "Interpret/rewtools.sml"
40 use "Interpret/script.sml"
41 use "Interpret/solve.sml"
42 use "Interpret/inform.sml"
43 use "Interpret/mathengine.sml"
45 use "xmlsrc/mathml.sml"
46 use "xmlsrc/datatypes.sml"
47 use "xmlsrc/pbl-met-hierarchy.sml"
48 use "xmlsrc/thy-hierarchy.sml"
49 use "xmlsrc/interface-xml.sml"
51 use "Frontend/messages.sml"
52 use "Frontend/states.sml"
53 use "Frontend/interface.sml"
56 ML {* writeln "**** build math-engine complete **************************" *}
58 ML {* writeln "**** build the Knowledge *********************************" *}
59 (*use_thy "Knowledge/Typefix" FIXXXMEWN100827*)
60 use_thy "Knowledge/Descript"
62 ML {* @{thm Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(26)} *}
64 ML {*"--------------------------------------------"*}
67 ML {*"--------------------------------------------"*}
77 use_thy "Knowledge/Atools"
80 use_thy "Knowledge/Simplify"
81 use_thy "Knowledge/Poly"
82 use_thy "Knowledge/Rational"
83 use_thy "Knowledge/PolyMinus"
84 use_thy "Knowledge/Equation"
85 use_thy "Knowledge/LinEq"
86 use_thy "Knowledge/Root"
87 use_thy "Knowledge/RootEq"
88 use_thy "Knowledge/RatEq"
89 use_thy "Knowledge/RootRat"
90 use_thy "Knowledge/RootRatEq"
91 use_thy "Knowledge/PolyEq"
92 use_thy "Knowledge/Vect"
93 use_thy "Knowledge/Calculus"
94 use_thy "Knowledge/Trig"
95 use_thy "Knowledge/LogExp"
96 use_thy "Knowledge/Diff"
97 use_thy "Knowledge/DiffApp"
98 use_thy "Knowledge/Integrate"
99 use_thy "Knowledge/EqSystem"
100 use_thy "Knowledge/Biegelinie"
101 use_thy "Knowledge/AlgEin"
102 use_thy "Knowledge/Test"
103 use_thy "Knowledge/Isac"