1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Tue May 19 12:33:35 2020 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Wed May 20 12:52:09 2020 +0200
     1.3 @@ -57,23 +57,25 @@
     1.4  
     1.5  theory Test_Isac_Short
     1.6    imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*)
     1.7 -  (* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one *)
     1.8 +  (* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one
     1.9 +     and find out, which ML_file or *.thy causes an error (might be ONLY one).
    1.10 +     Also backup files (#* ) recognised by jEdit cause this trouble                    *)
    1.11  (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
    1.12 -    "~~/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All"     (*broken with 05944144a692 *)
    1.13 -(**)"~~/test/Tools/isac/ADDTESTS/Ctxt"                       (*broken with 05944144a692 *)
    1.14 -(**)"~~/test/Tools/isac/ADDTESTS/test-depend/Build_Test"     (*broken with 05944144a692 *)
    1.15 -(**)"~~/test/Tools/isac/ADDTESTS/All_Ctxt"                   (*broken with 05944144a692 *)
    1.16 -(**)"~~/test/Tools/isac/ADDTESTS/Test_Units"                 (*broken with 05944144a692 *)
    1.17 -(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics"    (*broken with 05944144a692 *)
    1.18 -(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting" (*broken with 05944144a692 *)
    1.19 -(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"(*broken with 05944144a692 *)
    1.20 -(**)"~~/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test"    (*broken with 05944144a692 *)
    1.21 -(**)"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo"     (*broken with 05944144a692 *)
    1.22 +    "~~/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All"
    1.23 +(**)"~~/test/Tools/isac/ADDTESTS/Ctxt"
    1.24 +(**)"~~/test/Tools/isac/ADDTESTS/test-depend/Build_Test"
    1.25 +(**)"~~/test/Tools/isac/ADDTESTS/All_Ctxt"
    1.26 +(**)"~~/test/Tools/isac/ADDTESTS/Test_Units"
    1.27 +(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
    1.28 +(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
    1.29 +(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
    1.30 +(**)"~~/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
    1.31 +(**)"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo"
    1.32  (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
    1.33     ADDTESTS/------------------------------------------- see end of tests *)
    1.34  (*"~~/test/Pure/Isar/Test_Parsers"           dropped Isabelle2014-->2015 *)
    1.35  (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*)
    1.36 -(**)"~~/test/Pure/Isar/Test_Parse_Term"                      (*broken with 05944144a692 *)
    1.37 +(**)"~~/test/Pure/Isar/Test_Parse_Term"
    1.38  (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
    1.39    "~~/test/Tools/isac/Specify/refine"        (* setup for refine.sml   *)
    1.40    "~~/test/Tools/isac/ProgLang/calculate"    (* setup for evaluate.sml *)
    1.41 @@ -230,7 +232,6 @@
    1.42  subsection \<open>further functionality alongside batch build sequence\<close>
    1.43    ML_file "MathEngBasic/thmC.sml"
    1.44    ML_file "MathEngBasic/rewrite.sml"
    1.45 -(*ML_file "MathEngBasic/mstools.sml"*)
    1.46    ML_file "MathEngBasic/tactic.sml"
    1.47    ML_file "MathEngBasic/ctree.sml"
    1.48    ML_file "MathEngBasic/calculation.sml"