1 (* Title: build and test isac
2 Author: Walther Neuper, TU Graz, 100808
3 (c) due to copyright terms
5 $ cd /usr/local/Isabelle2009-1/src/Tools/isac
6 $ /usr/local/isabisac/bin/isabelle emacs Build_Isac.thy &
7 $ /usr/local/isabisac/bin/isabelle jedit Build_Isac.thy &
9 create a new Isac heap (via ~~/ROOT.ML) with
10 $ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac
13 $ /usr/local/isabisac/bin/isabelle emacs -l Isac Build_Isac.thy &
14 $ /usr/local/isabisac/bin/isabelle jedit -l Isac Build_Isac.thy &
16 12345678901234567890123456789012345678901234567890123456789012345678901234567890
17 10 20 30 40 50 60 70 80
20 header {* Loading the isac mathengine *}
23 (*imports Complex_Main "ProgLang/Language" (*"Knowledge/Isac"*)*)
28 tracing "**** build the isac kernel = math-engine + Knowledge ***********";
29 tracing "**** build the math-engine *************************************" *}
31 ML {* Toplevel.debug := true; *}
34 ML {* check_guhs_unique := true *}
36 use "ProgLang/termC.sml"
37 use "ProgLang/calculate.sml"
38 use "ProgLang/rewrite.sml"
39 use_thy"ProgLang/Script" (*ListC, Tools, Script*)
40 use "ProgLang/scrtools.sml"
41 use_thy"ProgLang/Language" (*just for integrating scrtools.sml*)
43 use "Interpret/mstools.sml"
44 use "Interpret/ctree.sml"
45 use "Interpret/ptyps.sml"
46 use "Interpret/generate.sml"
47 use "Interpret/calchead.sml"
48 use "Interpret/appl.sml"
49 use "Interpret/rewtools.sml"
50 use "Interpret/script.sml"
51 use "Interpret/solve.sml"
52 use "Interpret/inform.sml"
53 use "Interpret/mathengine.sml"
55 use "xmlsrc/mathml.sml"
56 use "xmlsrc/datatypes.sml"
57 use "xmlsrc/pbl-met-hierarchy.sml"
58 use "xmlsrc/thy-hierarchy.sml"
59 use "xmlsrc/interface-xml.sml"
61 use "Frontend/messages.sml"
62 use "Frontend/states.sml"
63 use "Frontend/interface.sml"
66 ML {* tracing "**** build math-engine complete **************************" *}
68 ML {* tracing "**** build the Knowledge *********************************" *}
69 (*use_thy "Knowledge/Delete"
70 use_thy "Knowledge/Descript"
71 use_thy "Knowledge/Atools"
72 use_thy "Knowledge/Simplify"
73 use_thy "Knowledge/Poly"
74 use_thy "Knowledge/Rational"
75 use_thy "Knowledge/PolyMinus"
76 use_thy "Knowledge/Equation"
77 use_thy "Knowledge/LinEq"
78 use_thy "Knowledge/Root"
79 use_thy "Knowledge/RootEq"
80 use_thy "Knowledge/RatEq"
81 use_thy "Knowledge/RootRat"
82 use_thy "Knowledge/RootRatEq"
83 use_thy "Knowledge/PolyEq"
84 use_thy "Knowledge/Vect"
85 use_thy "Knowledge/Calculus"
86 use_thy "Knowledge/Trig"
87 use_thy "Knowledge/LogExp"
88 use_thy "Knowledge/Diff"
89 use_thy "Knowledge/DiffApp"
90 use_thy "Knowledge/Integrate"
91 use_thy "Knowledge/EqSystem"
92 use_thy "Knowledge/Biegelinie"
93 use_thy "Knowledge/AlgEin"
95 use_thy "Knowledge/Test" (*required _only_ for ROOT.ML !?!*)
96 use_thy "Knowledge/Isac"
98 ML {* check_guhs_unique := false; *}
99 ML {* tracing "**** isac kernel = math-engine + Knowledge complete ******" *}
103 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
104 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)