test/Tools/isac/Test_Isac.thy
changeset 60028 bb97dcbf7360
parent 60024 4ccb7adf3448
child 60090 2f9e601d9e07
     1.1 --- a/test/Tools/isac/Test_Isac.thy	Thu Jul 02 09:57:58 2020 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Fri Jul 17 11:42:20 2020 +0200
     1.3 @@ -57,23 +57,24 @@
     1.4  
     1.5  theory Test_Isac
     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_Parsers"
    1.38 +(**)"~~/test/Pure/Isar/Test_Parse_Term"
    1.39  (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
    1.40    "~~/test/Tools/isac/Specify/refine"        (* setup for refine.sml   *)
    1.41    "~~/test/Tools/isac/ProgLang/calculate"    (* setup for evaluate.sml *)