tuned data structure

recovered level-free fishing for locale, accidentally lost in dce365931721

tuned terminology: emphasize stack-like nature of nested local theories

self-contained locale_declaration operation

yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo

tuned

recovered structure of module, which got somehow convoluted due to incremental modifications