test/Tools/isac/Test_Isac_Short.thy
changeset 59813 3b161c171472
parent 59804 403f00b309ef
child 59814 665dd868d4e2
     1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Thu Feb 20 18:47:55 2020 +0100
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Fri Feb 21 14:19:33 2020 +0100
     1.3 @@ -198,6 +198,7 @@
     1.4    ML_file "Minisubpbl/700-interSteps.sml"
     1.5    ML_file "Minisubpbl/790-complete-NEXT_STEP.sml"
     1.6    ML_file "Minisubpbl/790-complete.sml"
     1.7 +  ML_file "Minisubpbl/800-append-on-Frm.sml"
     1.8  
     1.9  subsection \<open>further functionality alongside batch build sequence\<close>
    1.10    ML_file "MathEngBasic/model.sml"
    1.11 @@ -214,7 +215,8 @@
    1.12    ML_file "Specify/appl.sml"          (*complete "WEGEN INTERMED TESTCODE"   *)
    1.13    ML_file "Specify/step-specify.sml"
    1.14    ML_file "Specify/specify.sml"
    1.15 -  ML_file "Interpret/rewtools.sml"                
    1.16 +
    1.17 +  ML_file "Interpret/rewtools.sml"
    1.18    ML_file "Interpret/li-tool.sml"
    1.19    ML_file "Interpret/inform.sml"
    1.20    ML_file "Interpret/lucas-interpreter.sml"