10 |
10 |
11 theory Test_Isac imports |
11 theory Test_Isac imports |
12 Isac |
12 Isac |
13 "Knowledge/Rational_Test" |
13 "Knowledge/Rational_Test" |
14 "ADDTESTS/Ctxt" |
14 "ADDTESTS/Ctxt" |
|
15 "ADDTESTS/test-depend/Build_Test" |
15 "ADDTESTS/All_Ctxt" |
16 "ADDTESTS/All_Ctxt" |
|
17 (*"ADDTESTS/course/T2_Rewriting" theory has not been declared*) |
|
18 (*"ADDTESTS/course/T1_Basics.thy" could not find ^^^*) |
|
19 (*"ADDTESTS/course/T3_MathEngine" could not find ^^^*) |
|
20 "ADDTESTS/file-depend/Build_Test" |
|
21 "../../Pure/Isar/Test_Parsers" |
|
22 (*"../../Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*) |
|
23 "../../Pure/Isar/Test_Parse_Term" |
16 |
24 |
17 uses |
25 uses |
18 ( "library.sml") |
26 ( "library.sml") |
19 ( "calcelems.sml") |
27 ( "calcelems.sml") |
20 ("ProgLang/termC.sml") |
28 ("ProgLang/termC.sml") |
129 use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*) |
137 use "xmlsrc/interface-xml.sml" (*TODO after 2009-2*) |
130 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*} |
138 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*} |
131 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*} |
139 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*} |
132 use "Frontend/messages.sml" (*new 2011*) |
140 use "Frontend/messages.sml" (*new 2011*) |
133 use "Frontend/states.sml" (*new 2011*) |
141 use "Frontend/states.sml" (*new 2011*) |
134 use "Frontend/interface.sml" (*part.*) |
142 use "Frontend/interface.sml" (*part.*) |
|
143 ML {* |
|
144 |
|
145 *} |
|
146 ML {* |
|
147 |
|
148 *} |
|
149 ML {* |
|
150 |
|
151 *} |
|
152 ML {* |
|
153 |
|
154 *} |
|
155 ML {* |
|
156 |
|
157 *} |
|
158 |
135 use "print_exn_G.sml" (*new 2011*) |
159 use "print_exn_G.sml" (*new 2011*) |
136 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*} |
160 ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*} |
137 ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*} |
161 ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*} |
138 use "Knowledge/delete.sml" (*new 2011*) |
162 use "Knowledge/delete.sml" (*new 2011*) |
139 use "Knowledge/descript.sml" (*new 2011*) |
163 use "Knowledge/descript.sml" (*new 2011*) |
169 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} |
193 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} |
170 ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*} |
194 ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*} |
171 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} |
195 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} |
172 |
196 |
173 ML {* |
197 ML {* |
|
198 "--------- mini-subpbl AUTO CompleteCalcHead ------------"; |
|
199 states:=[]; |
|
200 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], |
|
201 ("Test", ["sqroot-test","univariate","equation","test"], |
|
202 ["Test","squ-equ-test-subpbl1"]))]; |
|
203 Iterator 1; |
|
204 moveActiveRoot 1; |
|
205 (* doesn't terminate !!!*) |
|
206 autoCalculate 1 CompleteCalcHead; |
|
207 val (ModSpec (x1,x2,x3,x4,x5,x6), tac, asms) = pt_extract (pt, p); |
|
208 *} |
|
209 ML {* |
|
210 *} |
|
211 ML {* |
174 *} |
212 *} |
175 ML {* |
213 ML {* |
176 *} |
214 *} |
177 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} |
215 ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*} |
178 ML {* |
|
179 *} |
|
180 ML {* |
|
181 *} |
|
182 ML {* |
|
183 *} |
|
184 ML {* |
|
185 *} |
|
186 ML {* |
|
187 *} |
|
188 |
216 |
189 end |
217 end |
190 |
218 |
191 (*=== inhibit exn ?============================================================= |
219 (*=== inhibit exn ?============================================================= |
192 ===== inhibit exn ?===========================================================*) |
220 ===== inhibit exn ?===========================================================*) |
193 |
221 |
194 (*========== inhibit exn 110520 ================================================ |
222 (*========== inhibit exn 110620 ================================================ |
195 |
223 |
196 "########### testcode inserted vvv ###########################################"; |
224 "########### testcode inserted vvv ###########################################"; |
197 "########### testcode inserted ^^^ ###########################################"; |
225 "########### testcode inserted ^^^ ###########################################"; |
198 |
226 |
199 ============ inhibit exn 110520 ==============================================*) |
227 ============ inhibit exn 110620 ==============================================*) |
200 |
228 |
201 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
229 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
202 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) |
230 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) |
203 |
231 |