1.1 --- a/test/Tools/isac/Test_Isac.thy	Mon Nov 21 12:47:02 2016 +0100
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Tue Nov 22 10:42:21 2016 +0100
     1.3 @@ -20,9 +20,11 @@
     1.4  
     1.5  In order to maintain these tests without changes, this has to be done before running tests:
     1.6  (1) Query replace in src/Tools/isac:
     1.7 -    "--- ! aktivate for Test_Isac BEGIN ---\* )" \<longrightarrow> "--- ! aktivate for Test_Isac BEGIN ---\*)"
     1.8 -    "( *\--- ! aktivate for Test_Isac END ---"   \<longrightarrow> "(*\--- ! aktivate for Test_Isac END ---"
     1.9 -  This extends the signatures with some functions required for some tests.
    1.10 +    \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\* )\<clubsuit> \<longrightarrow> \<clubsuit>--- ! aktivate for Test_Isac BEGIN ---\*)\<clubsuit>
    1.11 +    \<clubsuit>( *\--- ! aktivate for Test_Isac END ---\<clubsuit>   \<longrightarrow> \<clubsuit>(*\--- ! aktivate for Test_Isac END ---\<clubsuit>
    1.12 +     ^^^ in signature outcommented,                     ^^^ NOT outcommented,
    1.13 +         this is status for coding                          this is status for tests
    1.14 +  "NOT outcommented" extends the signatures with some functions required for some tests.
    1.15  
    1.16  Running Test_Isac.thy opens all structures, see code after "begin" below.
    1.17  
    1.18 @@ -66,8 +68,9 @@
    1.19  
    1.20  ML {*
    1.21  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
    1.22 +  open Kernel;
    1.23 +  open Math_Engine
    1.24    open Lucin;
    1.25 -  open Kernel;
    1.26  (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.27  *}
    1.28  ML {*