equal
deleted
inserted
replaced
2507 end |
2507 end |
2508 (**) |
2508 (**) |
2509 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
2509 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
2510 open Ctree |
2510 open Ctree |
2511 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
2511 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
|
2512 |
|
2513 (* policy for "open" structures: |
|
2514 -------------------------------- |
|
2515 The above "open Ctree" creates an unclear situation with structures, in particular in test/. |
|
2516 This is work in progress, but urges to make policy explicit: |
|
2517 |
|
2518 (1) All structures are closed with a signature; this for prepares re-arrangement of structures. |
|
2519 (2) Some structures are pervasive (e.g. Ctree) such, that an "open" ensures readability locally. |
|
2520 (3) test/ is preceeded by "open" for all structures, in order to ease copy&paste from scr/ to test/ |
|
2521 |
|
2522 ad (1) Presently this point is under construction. |
|
2523 ad (2) Such local "open" are kept to a minimum (with the goal to reach Isabelle's state). |
|
2524 ad (3) See https://intra.ist.tugraz.at/hg/isa/file/2ba35efb07b7/test/Tools/isac/Test_Isac.thy#l70 |
|
2525 *) |