1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Tue Mar 03 11:59:06 2020 +0100
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Wed Mar 04 15:38:06 2020 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(* Title:  All tests on isac (some outcommented since Isabelle2002-->2009-2)
     1.5 +t(* Title:  All tests on isac (some outcommented since Isabelle2002-->2009-2)
     1.6     Author: Walther Neuper 101001
     1.7     (c) copyright due to license terms.
     1.8  
     1.9 @@ -91,6 +91,7 @@
    1.10    open Math_Engine;
    1.11    open Test_Code;              CalcTreeTEST;
    1.12    open LItool;                 itms2args;
    1.13 +  open Sub_Problem;
    1.14    open Step
    1.15    open Env;
    1.16    open LI;                     scan_dn;
    1.17 @@ -165,7 +166,7 @@
    1.18    ML_file "CalcElements/termC.sml"
    1.19    ML_file "CalcElements/contextC.sml"
    1.20    ML_file "CalcElements/environment.sml"
    1.21 -  ML_file "CalcElements/kestore.sml"        (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
    1.22 +  ML_file "CalcElements/kestore.sml"    (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
    1.23  (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
    1.24    ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
    1.25    ML_file "ProgLang/calculate.sml"      (* requires setup from calculate.thy                    *)
    1.26 @@ -218,6 +219,7 @@
    1.27    ML_file "Specify/step-specify.sml"
    1.28    ML_file "Specify/specify.sml"
    1.29  
    1.30 +  ML_file "Interpret/sub-problem.sml"
    1.31    ML_file "Interpret/rewtools.sml"
    1.32    ML_file "Interpret/li-tool.sml"
    1.33    ML_file "Interpret/inform.sml"