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 *)