226 ML_file "Minisubpbl/600-postcond.sml" |
226 ML_file "Minisubpbl/600-postcond.sml" |
227 ML_file "Minisubpbl/700-interSteps.sml" |
227 ML_file "Minisubpbl/700-interSteps.sml" |
228 ML_file "Minisubpbl/710-interSteps-short.sml" |
228 ML_file "Minisubpbl/710-interSteps-short.sml" |
229 ML_file "Minisubpbl/790-complete-NEXT_STEP.sml" |
229 ML_file "Minisubpbl/790-complete-NEXT_STEP.sml" |
230 ML_file "Minisubpbl/790-complete.sml" |
230 ML_file "Minisubpbl/790-complete.sml" |
231 ML_file "Minisubpbl/800-append-on-Frm.sml" |
231 ML_file "Minisubpbl/800-append-on-Frm.sml"(*STARTbroken with "reduce the number of TermC.parse*"*) |
232 |
232 |
233 subsection \<open>further functionality alongside batch build sequence\<close> |
233 subsection \<open>further functionality alongside batch build sequence\<close> |
234 ML_file "MathEngBasic/thmC.sml" |
234 ML_file "MathEngBasic/thmC.sml" |
235 ML_file "MathEngBasic/rewrite.sml" |
235 ML_file "MathEngBasic/rewrite.sml" |
236 ML_file "MathEngBasic/tactic.sml" |
236 ML_file "MathEngBasic/tactic.sml" |
237 (** )ML_file "MathEngBasic/ctree.sml" ( ** )loops with eliminate ThmC.numerals_to_Free*) |
237 (** )ML_file "MathEngBasic/ctree.sml" ( ** )loops with eliminate ThmC.numerals_to_Free*) |
238 ML_file "MathEngBasic/calculation.sml" |
238 ML_file "MathEngBasic/calculation.sml" |
239 |
239 |
240 ML_file "Specify/formalise.sml" |
240 ML_file "Specify/formalise.sml" |
252 ML_file "Specify/specify.sml" |
252 ML_file "Specify/specify.sml" |
253 ML_file "Specify/step-specify.sml" |
253 ML_file "Specify/step-specify.sml" |
254 |
254 |
255 ML_file "Interpret/istate.sml" |
255 ML_file "Interpret/istate.sml" |
256 ML_file "Interpret/sub-problem.sml" |
256 ML_file "Interpret/sub-problem.sml" |
257 ML_file "Interpret/error-pattern.sml" |
257 ML_file "Interpret/error-pattern.sml" (*broken with "reduce the number of TermC.parse*"*) |
258 ML_file "Interpret/li-tool.sml" |
258 ML_file "Interpret/li-tool.sml" |
259 ML_file "Interpret/lucas-interpreter.sml" |
259 ML_file "Interpret/lucas-interpreter.sml" (*broken with "reduce the number of TermC.parse*"*) |
260 ML_file "Interpret/step-solve.sml" |
260 ML_file "Interpret/step-solve.sml" |
261 |
261 |
262 ML_file "MathEngine/me-misc.sml" |
262 ML_file "MathEngine/me-misc.sml" |
263 ML_file "MathEngine/fetch-tactics.sml" |
263 ML_file "MathEngine/fetch-tactics.sml" |
264 ML_file "MathEngine/solve.sml" |
264 ML_file "MathEngine/solve.sml" |
265 ML_file "MathEngine/step.sml" |
265 ML_file "MathEngine/step.sml" |
266 ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*) |
266 ML_file "MathEngine/mathengine-stateless.sml" (*broken with "reduce the number of TermC.parse*"*) |
267 ML_file "MathEngine/messages.sml" |
267 ML_file "MathEngine/messages.sml" |
268 ML_file "MathEngine/states.sml" |
268 ML_file "MathEngine/states.sml" |
269 |
269 |
270 ML_file "BridgeLibisabelle/thy-present.sml" |
270 ML_file "BridgeLibisabelle/thy-present.sml" |
271 ML_file "BridgeLibisabelle/mathml.sml" (*part.*) |
271 ML_file "BridgeLibisabelle/mathml.sml" (*part.*) |
278 ML_file "BridgeJEdit/preliminary.sml" |
278 ML_file "BridgeJEdit/preliminary.sml" |
279 |
279 |
280 ML_file "Knowledge/delete.sml" |
280 ML_file "Knowledge/delete.sml" |
281 ML_file "Knowledge/descript.sml" |
281 ML_file "Knowledge/descript.sml" |
282 ML_file "Knowledge/simplify.sml" |
282 ML_file "Knowledge/simplify.sml" |
283 ML_file "Knowledge/poly-1.sml" |
283 (* ML_file "Knowledge/poly-1.sml" broken with "reduce the number of TermC.parse*"*) |
284 (*ML_file "Knowledge/poly-2.sml" Test_Isac_Short*) |
284 (*ML_file "Knowledge/poly-2.sml" Test_Isac_Short*) |
285 ML_file "Knowledge/gcd_poly_ml.sml" |
285 ML_file "Knowledge/gcd_poly_ml.sml" |
286 ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*) |
286 ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*) |
287 ML_file "Knowledge/rational-1.sml" |
287 ML_file "Knowledge/rational-1.sml" |
288 (*ML_file "Knowledge/rational-2.sml" Test_Isac_Short*) |
288 (*ML_file "Knowledge/rational-2.sml" Test_Isac_Short*) |
320 ML_file "Knowledge/build_thydata.sml" |
320 ML_file "Knowledge/build_thydata.sml" |
321 |
321 |
322 ML_file "Test_Code/test-code.sml" |
322 ML_file "Test_Code/test-code.sml" |
323 |
323 |
324 section \<open>further tests additional to src/.. files\<close> |
324 section \<open>further tests additional to src/.. files\<close> |
325 ML_file "BridgeLibisabelle/use-cases.sml" |
325 (*ML_file "BridgeLibisabelle/use-cases.sml" broken with "reduce the number of TermC.parse*"*) |
|
326 ML \<open> |
|
327 \<close> ML \<open> |
|
328 (*TOODOO broken with "reduce the number of TermC.parse---------------------------------------\\*" |
|
329 TOODOObroken with "reduce the number of TermC.parse*"--------------------------------------//*) |
|
330 \<close> ML \<open> |
|
331 \<close> ML \<open> |
|
332 \<close> ML \<open> |
|
333 \<close> ML \<open> |
|
334 \<close> ML \<open> |
|
335 \<close> ML \<open> |
|
336 \<close> ML \<open> |
|
337 \<close> ML \<open> |
|
338 \<close> ML \<open> |
|
339 \<close> |
326 |
340 |
327 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
341 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
328 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
342 ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
329 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
343 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
330 ML \<open> |
344 ML \<open> |