1.1 --- a/test/Tools/isac/Test_Isac.thy Thu Oct 22 14:03:40 2020 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Oct 22 15:40:41 2020 +0200
1.3 @@ -73,6 +73,14 @@
1.4 (**)"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo"
1.5 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
1.6 ADDTESTS/------------------------------------------- see end of tests *)
1.7 +(*/--- these work directly from Pure, but create problems here ..
1.8 + "~~/test/Pure/Isar/Keyword_ISAC.thy" (* Malformed theory import, "keywords" ?!? *)
1.9 + "~~/test/Pure/Isar/Test_Parse_Isac.thy" (* Malformed theory import, "keywords" ?!? *)
1.10 + "~~/test/Pure/Isar/Test_Parsers_Cookbook.thy" (* Malformed theory import ?!? *)
1.11 + "~~/test/Pure/Isar/Theory_Commands" (*Duplicate outer syntax command "ISAC" *)
1.12 + \--- .. these work independently, but create problems here *)
1.13 +(**)"~~/test/Pure/Isar/Check_Outer_Syntax"
1.14 +(** )"~~/test/Pure/Isar/Downto_Synchorinzed"( *TODO: errors to resolve*)
1.15 (**)"~~/test/Pure/Isar/Test_Parsers"
1.16 (**)"~~/test/Pure/Isar/Test_Parse_Term"
1.17 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
1.18 @@ -231,7 +239,6 @@
1.19 subsection \<open>further functionality alongside batch build sequence\<close>
1.20 ML_file "MathEngBasic/thmC.sml"
1.21 ML_file "MathEngBasic/rewrite.sml"
1.22 -(*ML_file "MathEngBasic/mstools.sml"*)
1.23 ML_file "MathEngBasic/tactic.sml"
1.24 ML_file "MathEngBasic/ctree.sml"
1.25 ML_file "MathEngBasic/calculation.sml"
1.26 @@ -276,6 +283,8 @@
1.27 (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
1.28 ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
1.29
1.30 + ML_file "BridgeJEdit/parseC.sml"
1.31 +
1.32 ML_file "Knowledge/delete.sml"
1.33 ML_file "Knowledge/descript.sml"
1.34 ML_file "Knowledge/simplify.sml"