1.1 --- a/src/Tools/isac/Interpret/ctree.sml	Thu Dec 22 10:39:45 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Thu Dec 22 11:12:18 2016 +0100
     1.3 @@ -2509,3 +2509,17 @@
     1.4  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     1.5  open Ctree
     1.6  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
     1.7 +
     1.8 +(* policy for "open" structures:
     1.9 +--------------------------------
    1.10 +The above "open Ctree" creates an unclear situation with structures, in particular in test/.
    1.11 +This is work in progress, but urges to make policy explicit:
    1.12 +
    1.13 +(1) All structures are closed with a signature; this for prepares re-arrangement of structures.
    1.14 +(2) Some structures are pervasive (e.g. Ctree) such, that an "open" ensures readability locally.
    1.15 +(3) test/ is preceeded by "open" for all structures, in order to ease copy&paste from scr/ to test/
    1.16 +
    1.17 +ad (1) Presently this point is under construction.
    1.18 +ad (2) Such local "open" are kept to a minimum (with the goal to reach Isabelle's state).
    1.19 +ad (3) See https://intra.ist.tugraz.at/hg/isa/file/2ba35efb07b7/test/Tools/isac/Test_Isac.thy#l70
    1.20 +*)