1.1 --- a/test/Tools/isac/Test_Isac.thy	Sat May 09 15:31:15 2020 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Sun May 10 13:16:56 2020 +0200
     1.3 @@ -7,6 +7,8 @@
     1.4     plus
     1.5       ~~/test/Tools/isac/ADDTESTS
     1.6       ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
     1.7 +
     1.8 +Note, that only the first error in a file is shown here.
     1.9  *)
    1.10  
    1.11  section \<open>Notes on running tests\<close>
    1.12 @@ -112,12 +114,10 @@
    1.13    open Input_Descript;
    1.14    open Specify;                show_ptyps;
    1.15    open SpecifyNEW;
    1.16 -  open ApplicableOLD;             mk_set;
    1.17    open Step_Specify;
    1.18    open Step_Solve;
    1.19    open Step;
    1.20    open Solve;                  (* NONE *)
    1.21 -  open Selem;                  Formalise.empty;
    1.22    open Stool;                  (* NONE *)
    1.23    open ContextC;               transfer_asms_from_to;
    1.24    open Tactic;                 (* NONE *)
    1.25 @@ -186,7 +186,7 @@
    1.26    ML_file "BaseDefinitions/error-fill-def.sml"
    1.27    ML_file "BaseDefinitions/rule-set.sml"
    1.28    ML_file "BaseDefinitions/check-unique.sml"
    1.29 -(*called by Know_Store*)
    1.30 +(*called by Know_Store..*)
    1.31    ML_file "BaseDefinitions/calcelems.sml"
    1.32    ML_file "BaseDefinitions/termC.sml"
    1.33    ML_file "BaseDefinitions/substitution.sml"
    1.34 @@ -195,6 +195,7 @@
    1.35    ML_file "BaseDefinitions/kestore.sml"    (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
    1.36  (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
    1.37    ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
    1.38 +
    1.39    ML_file "ProgLang/evaluate.sml"      (* requires setup from calculate.thy                    *)
    1.40    ML_file "ProgLang/listC.sml"
    1.41    ML_file "ProgLang/prog_expr.sml"
    1.42 @@ -233,11 +234,12 @@
    1.43    ML_file "MathEngBasic/rewrite.sml"
    1.44    ML_file "MathEngBasic/model.sml"
    1.45    ML_file "MathEngBasic/mstools.sml"
    1.46 -  ML_file "MathEngBasic/specification-elems.sml"
    1.47    ML_file "MathEngBasic/tactic.sml"
    1.48    ML_file "MathEngBasic/ctree.sml"
    1.49    ML_file "MathEngBasic/calculation.sml"
    1.50  
    1.51 +  ML_file "Specify/o-model.sml"
    1.52 +  ML_file "Specify/i-model.sml"
    1.53    ML_file "Specify/ptyps.sml"         (* requires setup from ptyps.thy *)
    1.54    ML \<open>(*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*)\<close>
    1.55    ML_file "Specify/generate.sml"