|
1 (* Title: Run_Tests as long Isac is not available: REPLACE 'IMPORTS' |
|
2 Author: Walther Neuper 101001 |
|
3 (c) copyright due to lincense terms. |
|
4 |
|
5 $ cd /usr/local/isabisac/test/Tools/isac |
|
6 $ /usr/local/isabisac/bin/isabelle emacs Test_Some.thy & |
|
7 *) |
|
8 |
|
9 theory Test_Isac imports Isac |
|
10 "ProgLang/ProgLang" |
|
11 "Interpret/Interpret" |
|
12 "xmlsrc/xmlsrc" |
|
13 "Frontend/Frontend" |
|
14 "Knowledge/Knowledge" |
|
15 begin |
|
16 (* cd "systest"; |
|
17 (*+ check kbtest/diffapp.sml for additional items in met-model*) |
|
18 use"root-equ.sml"; |
|
19 use"script.sml"; |
|
20 (* use"script_if.sml"; WN03 missing: is_rootequation_in*) |
|
21 use"scriptnew.sml"; |
|
22 use"subp-rooteq.sml"; |
|
23 use"tacis.sml"; |
|
24 use"interface-xml.sml"; |
|
25 (* use"testdaten.sml"; no update after dropping 'errorBound'*) |
|
26 cd "../.."; |
|
27 *) |
|
28 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*} |
|
29 use "library.sml" (*new 2011*) |
|
30 use "calcelems.sml" (*complete*) |
|
31 use "ProgLang/termC.sml" (*part.*) |
|
32 use "ProgLang/calculate.sml" (*part.*) |
|
33 use "ProgLang/rewrite.sml" (*part.*) |
|
34 (*use "ProgLang/listg.sml" 2002*) |
|
35 (*use "ProgLang/scrtools.sml" 2002*) |
|
36 (*use "ProgLang/tools.sml" 2002*) |
|
37 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*} |
|
38 |
|
39 (*??? "ProgLang/ProgLang"*) |
|
40 |
|
41 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*} |
|
42 use "Interpret/mstools.sml" (*empty*) |
|
43 (*use "Interpret/ctree.sml" TODO*) |
|
44 use "Interpret/ptyps.sml" (* *) |
|
45 (*use "Interpret/generate.sml" new 2011*) |
|
46 use "Interpret/calchead.sml" (* *) |
|
47 (*use "Interpret/appl.sml" new 2011*) |
|
48 use "Interpret/rewtools.sml" (* *) |
|
49 (*use "Interpret/script.sml" TODO*) |
|
50 (*use "Interpret/solve.sml" TODO*) |
|
51 (*use "Interpret/inform.sml" TODO*) |
|
52 use "Interpret/mathengine.sml"(*part.*) |
|
53 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*} |
|
54 |
|
55 (*??? "Interpret/Interpret"*) |
|
56 |
|
57 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*} |
|
58 (*use "xmlsrc/mathml.sml" TODO*) |
|
59 (*use "xmlsrc/datatypes.sml" TODO*) |
|
60 (*use "xmlsrc/pbl-met-hierarchy.sml" TODO*) |
|
61 (*use "xmlsrc/thy-hierarchy.sml" TODO after 2009-2*) |
|
62 use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*) |
|
63 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*} |
|
64 |
|
65 (*??? "xmlsrc/xmlsrc"*) |
|
66 |
|
67 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*} |
|
68 use "Frontend/messages.sml" (*new 2011*) |
|
69 use "Frontend/states.sml" (*new 2011*) |
|
70 use "Frontend/interface.sml" (*part.*) |
|
71 |
|
72 use "print_exn_G.sml" (*new 2011*) |
|
73 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*} |
|
74 |
|
75 (*??? "Frontend/Frontend"*) |
|
76 |
|
77 ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*} |
|
78 use "Knowledge/delete.sml" (*new 2011*) |
|
79 use "Knowledge/descript.sml" (*new 2011*) |
|
80 (*use "Knowledge/atools.sml" 2002, added termorder.sml 2011*) |
|
81 use "Knowledge/simplify.sml" (*part.*) |
|
82 (*use "Knowledge/poly.sml" 2002*) |
|
83 use "Knowledge/rational.sml" (*part.*) |
|
84 (*use "Knowledge/equation.sml" 2002*) |
|
85 (*use "Knowledge/root.sml" 2002*) |
|
86 use "Knowledge/lineq.sml" (*new 2011*) |
|
87 (*use "Knowledge/rooteq.sml" 2002*) |
|
88 (*use "Knowledge/rateq.sml" 2002*) |
|
89 (*use "Knowledge/rootrat.sml" 2002*) |
|
90 (*use "Knowledge/rootrateq.sml" 2002*) |
|
91 (*use "Knowledge/polyeq.sml" 2002*) |
|
92 use "Knowledge/calculus.sml" (*new 2011*) |
|
93 (*use "Knowledge/trig.sml" 2002*) |
|
94 (*use "Knowledge/logexp.sml" 2002*) |
|
95 use "Knowledge/diff.sml" (*part.*) |
|
96 use "Knowledge/integrate.sml" (*part. was complete 2009-2*) |
|
97 (*use "Knowledge/eqsystem.sml" 2002*) |
|
98 use "Knowledge/test.sml" (*new 2011*) |
|
99 use "Knowledge/polyminus.sml" (*part.*) |
|
100 (*use "Knowledge/vect.sml" 2002*) |
|
101 (*use "Knowledge/diffapp.sml" 2002*) |
|
102 (*use "Knowledge/biegelinie.sml" 2002*) |
|
103 (*use "Knowledge/algein.sml" 2002*) |
|
104 use "Knowledge/diophanteq.sml" (*complete*) |
|
105 use "Knowledge/isac.sml" (*part.*) |
|
106 ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*} |
|
107 |
|
108 (*??? "Knowledge/Knowledge"*) |
|
109 |
|
110 end |
|
111 |
|
112 |
|
113 (*=== inhibit exn ?============================================================= |
|
114 ===== inhibit exn ?===========================================================*) |
|
115 |
|
116 |
|
117 (*========== inhibit exn 110317 ================================================ |
|
118 |
|
119 "########### testcode inserted vvv ###########################################"; |
|
120 "########### testcode inserted ^^^ ###########################################"; |
|
121 |
|
122 ============ inhibit exn 110317 ==============================================*) |
|
123 |
|
124 |
|
125 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
|
126 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) |