Changes

Summary

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