Changes

Summary

1. removed unused option, which is potentially expensive;
2. allow to augment session context via explicit session infos; more compact required_session interface;
3. synthesize session with all required theories from other session imports;
4. clarified signature;
5. clarified signature;
6. clarified signature;
7. clarified signature;
8. clarified signature: global_theories is always required;
9. tuned;
10. tuned signature;
11. clarified modules;
12. minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
13. more permissive: db could be empty after hard crash;
14. no censorship (in contrast to 2c828c830ad7);
15. A few more topological results. And made some slow proofs faster
16. removed ancient nat-int transfer
17. added lemma