Changes

Summary

1. more robust: avoid crash of AFP/Transition_Systems_and_Automata (amending fe4bd39bfeac and 43d8385db923);
2. more robust: zproofs need to be enabled (amending 43d8385db923);
3. more thorough thm definition via Global_Theory.register_proofs: store (and purge) zproofs;
4. tuned names;
5. clarified signature: support update of local_theory;
6. tuned;
7. clarified modules;
8. tuned;
9. unused;
10. clarified modules;
11. tuned;
12. clarified modules;
13. tuned;
14. tuned signature;
15. tuned;
16. more operations;