test/Tools/isac/Test_Isac_Short.thy
changeset 60090 2f9e601d9e07
parent 60084 3b1c95576911
child 60095 5fcd4f0c3886
     1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Thu Oct 22 14:03:40 2020 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Thu Oct 22 15:40:41 2020 +0200
     1.3 @@ -73,12 +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 independently, but create problems here ..
     1.8 +(*/--- these work directly from Pure, but create problems here ..
     1.9    "~~/test/Pure/Isar/Keyword_ISAC.thy"           (* Malformed theory import, "keywords" ?!? *)
    1.10 -  "~~/test/Pure/Isar/Keywords_Diag.thy"          (* Malformed theory import, "keywords" ?!? *)
    1.11    "~~/test/Pure/Isar/Test_Parse_Isac.thy"        (* Malformed theory import, "keywords" ?!? *)
    1.12    "~~/test/Pure/Isar/Test_Parsers_Cookbook.thy"  (* Malformed theory import             ?!? *)
    1.13 +  "~~/test/Pure/Isar/Theory_Commands"            (*Duplicate outer syntax command "ISAC"    *)
    1.14    \--- .. these work independently, but create problems here *)
    1.15 +(**)"~~/test/Pure/Isar/Check_Outer_Syntax"
    1.16 +(** )"~~/test/Pure/Isar/Downto_Synchorinzed"( *TODO: errors to resolve*)
    1.17  (**)"~~/test/Pure/Isar/Test_Parsers"
    1.18  (**)"~~/test/Pure/Isar/Test_Parse_Term"
    1.19  (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
    1.20 @@ -311,7 +313,7 @@
    1.21    ML_file "Knowledge/polyminus.sml"
    1.22    ML_file "Knowledge/vect.sml"
    1.23    ML_file "Knowledge/diffapp.sml"        (* postponed to dev. specification | TP-prog. *)
    1.24 -  ML_file "Knowledge/biegelinie-1.sml" 
    1.25 +  ML_file "Knowledge/biegelinie-1.sml"
    1.26  (*ML_file "Knowledge/biegelinie-2.sml"                                          Test_Isac_Short*)
    1.27  (*ML_file "Knowledge/biegelinie-3.sml"                                          Test_Isac_Short*)
    1.28    ML_file "Knowledge/biegelinie-4.sml"
    1.29 @@ -332,7 +334,7 @@
    1.30    ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
    1.31    ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
    1.32    ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
    1.33 -ML \<open> 
    1.34 +ML \<open>
    1.35  \<close> ML \<open>
    1.36  \<close> ML \<open>
    1.37  \<close> ML \<open>