test/Tools/isac/Test_Isac.thy
changeset 59410 2cbb98890190
parent 59403 ff716184230f
child 59411 3e241a6938ce
     1.1 --- a/test/Tools/isac/Test_Isac.thy	Thu Mar 15 15:26:06 2018 +0100
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Thu Mar 15 15:48:52 2018 +0100
     1.3 @@ -54,7 +54,7 @@
     1.4  * watch the <Theories> window for errors in the "imports" below
     1.5  \<close>
     1.6  
     1.7 -theory Test_Isac imports Build_Thydata
     1.8 +theory Test_Isac imports Build_Thydata (* note that imports are WITHOUT open struct ..*)
     1.9  (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
    1.10    "ADDTESTS/accumulate-val/Thy_All"
    1.11    "ADDTESTS/Ctxt"
    1.12 @@ -108,7 +108,8 @@
    1.13    open LTool;                  rule2stac;
    1.14    open Rewrite;                mk_thm;
    1.15    open Calc;                   get_pair;
    1.16 -  open TermC;                  ;
    1.17 +  open TermC;                  atomt;
    1.18 +  open Celem;                  terms2strs;
    1.19  (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.20  *}
    1.21