Summary
- tuned
- more structural sharing between common target Generic_Target.init
- exit always refers to the bottom of a nested local theory stack, after_close always to all non-bottom elements
- treat exit separate from regular local theory operations
- provide explicit variant initializers for regular named target vs. almost-named target
- prefer explicit datatype over implicit sum; given up separate implementation to pretty-print locale specifications
- compactified output