test/Tools/isac/Test_Isac_Short.thy
changeset 60624 0e0ac7706f0d
parent 60610 798e54862b08
child 60629 20c3d272d79c
     1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Fri Dec 09 16:29:04 2022 +0100
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Thu Dec 15 13:03:51 2022 +0100
     1.3 @@ -206,10 +206,11 @@
     1.4    ML_file "BaseDefinitions/libraryC.sml"
     1.5    ML_file "BaseDefinitions/rule-def.sml"
     1.6    ML_file "BaseDefinitions/eval-def.sml"
     1.7 -  ML_file "BaseDefinitions/rewrite-order.sml"                    
     1.8 +  ML_file "BaseDefinitions/rewrite-order.sml"
     1.9    ML_file "BaseDefinitions/theoryC.sml"
    1.10    ML_file "BaseDefinitions/rule.sml"
    1.11    ML_file "BaseDefinitions/thmC-def.sml"
    1.12 +  ML_file "BaseDefinitions/model-pattern.sml"
    1.13    ML_file "BaseDefinitions/error-fill-def.sml"
    1.14    ML_file "BaseDefinitions/rule-set.sml"
    1.15    ML_file "BaseDefinitions/check-unique.sml"
    1.16 @@ -260,6 +261,7 @@
    1.17  
    1.18  subsection \<open>further functionality alongside batch build sequence\<close>
    1.19    ML_file "MathEngBasic/thmC.sml"
    1.20 +  ML_file "MathEngBasic/problem.sml"
    1.21    ML_file "MathEngBasic/rewrite.sml"
    1.22    ML_file "MathEngBasic/tactic.sml"
    1.23    ML_file "MathEngBasic/ctree.sml" (*if red, get the file into a text buffer -- this might clear*)
    1.24 @@ -291,7 +293,7 @@
    1.25    ML_file "MathEngine/fetch-tactics.sml"
    1.26    ML_file "MathEngine/solve.sml"
    1.27    ML_file "MathEngine/step.sml"
    1.28 -  ML_file "MathEngine/mathengine-stateless.sml"    (*!part. WN130804: +check Interpret/me.sml*)
    1.29 +  ML_file "MathEngine/mathengine-stateless.sml"
    1.30    ML_file "MathEngine/messages.sml"
    1.31    ML_file "MathEngine/states.sml"
    1.32  
    1.33 @@ -334,7 +336,7 @@
    1.34    ML_file "Knowledge/eqsystem-1a.sml"
    1.35    ML_file "Knowledge/eqsystem-2.sml"
    1.36    ML_file "Knowledge/test.sml"
    1.37 -  ML_file "Knowledge/polyminus.sml"     
    1.38 +  ML_file "Knowledge/polyminus.sml"
    1.39    ML_file "Knowledge/vect.sml"
    1.40    ML_file "Knowledge/diff-app.sml"        (* postponed to dev. specification | TP-prog. *)
    1.41    ML_file "Knowledge/biegelinie-1.sml"