Changes

Summary

1. merged
2. more horrible proofs disentangled
3. tuned
4. more structural sharing between common target Generic_Target.init
5. exit always refers to the bottom of a nested local theory stack, after_close always to all non-bottom elements
6. treat exit separate from regular local theory operations
7. provide explicit variant initializers for regular named target vs. almost-named target
8. prefer explicit datatype over implicit sum; given up separate implementation to pretty-print locale specifications
9. compactified output
10. lifting setup for char
11. one single plugin for code type declarations avoids problems when bootstrapping new plugins over types which have been both declared concrete and abstract in their code historiy
12. uniform namespace handling for both concrete and abstract types, following 32e0da92c786
13. clarified
14. corrected slip
15. tuned
16. work around weakness in export calculation when generating OCaml code
17. tuned