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