1.1 --- a/test/Tools/isac/Test_Isac.thy	Mon May 18 14:21:41 2020 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Tue May 19 12:33:35 2020 +0200
     1.3 @@ -235,15 +235,20 @@
     1.4    ML_file "MathEngBasic/ctree.sml"
     1.5    ML_file "MathEngBasic/calculation.sml"
     1.6  
     1.7 +  ML_file "Specify/formalise.sml"
     1.8    ML_file "Specify/o-model.sml"
     1.9    ML_file "Specify/i-model.sml"
    1.10 +  ML_file "Specify/pre-conditions.sml"
    1.11 +  ML_file "Specify/p-model.sml"
    1.12    ML_file "Specify/m-match.sml"
    1.13    ML_file "Specify/refine.sml"        (* requires setup from refine.thy *)
    1.14 -  ML_file "Specify/ptyps.sml" 
    1.15 -  ML \<open>(*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*)\<close>
    1.16 -  ML_file "Specify/calchead.sml"
    1.17 +  ML_file "Specify/test-out.sml"
    1.18 +  ML_file "Specify/specify-step.sml"
    1.19 +  ML_file "Specify/specification.sml"
    1.20 +  ML_file "Specify/cas-command.sml"
    1.21 +  ML_file "Specify/p-spec.sml"
    1.22 +  ML_file "Specify/specify.sml"
    1.23    ML_file "Specify/step-specify.sml"
    1.24 -  ML_file "Specify/specify.sml"
    1.25  
    1.26    ML_file "Interpret/istate.sml"
    1.27    ML_file "Interpret/sub-problem.sml"
    1.28 @@ -252,6 +257,7 @@
    1.29    ML_file "Interpret/lucas-interpreter.sml"
    1.30    ML_file "Interpret/step-solve.sml"
    1.31  
    1.32 +  ML_file "MathEngine/me-misc.sml"
    1.33    ML_file "MathEngine/fetch-tactics.sml"
    1.34    ML_file "MathEngine/solve.sml"
    1.35    ML_file "MathEngine/step.sml"