Changes

Summary

1. tuned comments (see also 476a239d3e0e and possibly 4b62e0cb3aa8);
2. merged
3. minor performance tuning;
4. tuned;
5. minor performance tuning: prefer Same.operation;
6. clarified signature; minor performance tuning: avoid redundant identity;
7. minor performance tuning;
8. more operations;
9. revert 17fda85a33dc: renaming is not necessarily unique, e.g. [("x", "x"), ("x", "y")];
10. misc tuning and clarification;
11. minor performance tuning: prefer Symset.T; tuned names;
12. minor performace tuning;
13. minor performance tuning: prefer Same.operation;
14. tuned: more standard accumulation;
15. tuned;
16. clarified modules;
17. clarified signature;
18. tuned whitespace;
19. tuned;
20. proper ZTerm.lift_proof (amending 4a1a25bdf81d);
21. filter predecessors properly (amending ee405c40db72);
22. improve graphical clarity by omitting intra-host dependencies (following ee405c40db72);
23. more zproofs;
24. minor performance tuning: more direct abstraction level;
25. more general Logic.incr_indexes_operation; more special Logic.incr_indexes;
26. tuned;
27. tuned;
28. clarified modules;
29. clarified ML;
30. clarified signature; minor performance tuning;
31. tuned signature;
32. avoid accidental capture of theory value, and thus reduce heap size again (amending 5109e4b2a292);
33. tuned;
34. more robust: proper Proofterm.get_proofs_level with bound check;
35. tuned;
36. clarified signature: fewer tuples;
37. clarified signature: fewer tuples;
38. clarified signature: more explicit get_proofs_level with bounds check;