1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Mon Apr 19 20:31:24 2021 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Mon Apr 19 20:33:04 2021 +0200
     1.3 @@ -17,17 +17,6 @@
     1.4    Isac encapsulates code as much as possible in structures without open.
     1.5    This policy conflicts with those tests, which go into functions to details
     1.6    not declared in the signatures.
     1.7 -  
     1.8 -  In order to maintain these tests without changes, this has to be done before running tests:
     1.9 -  (1) Extend signatures for tests by
    1.10 -      ~~$ ./xcoding-to-test.sh
    1.11 -      ~~$ ./zcoding-to-test.sh  # --"-- + go back to Test_Isac.thy
    1.12 -      Running Test_Isac.thy opens all structures, see code after "begin" below.
    1.13 -  (2) Clean signatures for coding
    1.14 -      ~~$ ./xtest-to-coding.sh
    1.15 -      ~~$ ./ztest-to-coding.sh  # --"-- + go back to coding (!update thy!)
    1.16 -
    1.17 -//******************* don't forget (2) BEFORE pushing to repository **************************\\
    1.18  \<close>
    1.19  subsection \<open>Decide between running Test_Isac_Short.thy and Test_Isac.thy\<close>
    1.20  text \<open>