test/Tools/isac/Test_Isac.thy
changeset 60090 2f9e601d9e07
parent 60028 bb97dcbf7360
child 60095 5fcd4f0c3886
     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"