Changes

Summary

1. clarified signature: prefer explicit combinator;
2. unused;
3. restore heaps from database, which takes precedence over file-system;
4. tuned;
5. more operations;
6. tuned;
7. more robust try-finally;
8. tuned signature;
9. proper clean_entry;
10. afford larger build_database_slice for better compression (HOL: 1 slice, HOL-Proofs: multiple slices for testing);
11. prefer system option;
12. clarified signature: more explicit class SQL.Data;
13. proper ML_Heap.clean_entry;
14. tuned signature;
15. tuned;
16. store heaps within database server;
17. tuned signature;
18. clarified modules;
19. tuned signature;
20. clarified modules;
21. clarified modules;