233 (*ML_file "MathEngBasic/mstools.sml"*) |
233 (*ML_file "MathEngBasic/mstools.sml"*) |
234 ML_file "MathEngBasic/tactic.sml" |
234 ML_file "MathEngBasic/tactic.sml" |
235 ML_file "MathEngBasic/ctree.sml" |
235 ML_file "MathEngBasic/ctree.sml" |
236 ML_file "MathEngBasic/calculation.sml" |
236 ML_file "MathEngBasic/calculation.sml" |
237 |
237 |
|
238 ML_file "Specify/formalise.sml" |
238 ML_file "Specify/o-model.sml" |
239 ML_file "Specify/o-model.sml" |
239 ML_file "Specify/i-model.sml" |
240 ML_file "Specify/i-model.sml" |
|
241 ML_file "Specify/pre-conditions.sml" |
|
242 ML_file "Specify/p-model.sml" |
240 ML_file "Specify/m-match.sml" |
243 ML_file "Specify/m-match.sml" |
241 ML_file "Specify/refine.sml" (* requires setup from refine.thy *) |
244 ML_file "Specify/refine.sml" (* requires setup from refine.thy *) |
242 ML_file "Specify/ptyps.sml" |
245 ML_file "Specify/test-out.sml" |
243 ML \<open>(*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*)\<close> |
246 ML_file "Specify/specify-step.sml" |
244 ML_file "Specify/calchead.sml" |
247 ML_file "Specify/specification.sml" |
|
248 ML_file "Specify/cas-command.sml" |
|
249 ML_file "Specify/p-spec.sml" |
|
250 ML_file "Specify/specify.sml" |
245 ML_file "Specify/step-specify.sml" |
251 ML_file "Specify/step-specify.sml" |
246 ML_file "Specify/specify.sml" |
|
247 |
252 |
248 ML_file "Interpret/istate.sml" |
253 ML_file "Interpret/istate.sml" |
249 ML_file "Interpret/sub-problem.sml" |
254 ML_file "Interpret/sub-problem.sml" |
250 ML_file "Interpret/error-pattern.sml" |
255 ML_file "Interpret/error-pattern.sml" |
251 ML_file "Interpret/li-tool.sml" |
256 ML_file "Interpret/li-tool.sml" |
252 ML_file "Interpret/lucas-interpreter.sml" |
257 ML_file "Interpret/lucas-interpreter.sml" |
253 ML_file "Interpret/step-solve.sml" |
258 ML_file "Interpret/step-solve.sml" |
254 |
259 |
|
260 ML_file "MathEngine/me-misc.sml" |
255 ML_file "MathEngine/fetch-tactics.sml" |
261 ML_file "MathEngine/fetch-tactics.sml" |
256 ML_file "MathEngine/solve.sml" |
262 ML_file "MathEngine/solve.sml" |
257 ML_file "MathEngine/step.sml" |
263 ML_file "MathEngine/step.sml" |
258 ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*) |
264 ML_file "MathEngine/mathengine-stateless.sml" (*!part. WN130804: +check Interpret/me.sml*) |
259 ML_file "MathEngine/messages.sml" |
265 ML_file "MathEngine/messages.sml" |