minor performance tuning;

more operations;

revert 17fda85a33dc: renaming is not necessarily unique, e.g. [("x", "x"), ("x", "y")];

misc tuning and clarification;

minor performance tuning: prefer Symset.T; tuned names;

minor performace tuning;

minor performance tuning: prefer Same.operation;

tuned: more standard accumulation;

tuned;

clarified modules;

clarified signature;

tuned whitespace;

tuned;

proper ZTerm.lift_proof (amending 4a1a25bdf81d);

filter predecessors properly (amending ee405c40db72);

improve graphical clarity by omitting intra-host dependencies (following ee405c40db72);

more zproofs;

minor performance tuning: more direct abstraction level;

more general Logic.incr_indexes_operation; more special Logic.incr_indexes;

tuned;

tuned;

clarified modules;

clarified ML;

clarified signature; minor performance tuning;

tuned signature;

avoid accidental capture of theory value, and thus reduce heap size again (amending 5109e4b2a292);

tuned;

more robust: proper Proofterm.get_proofs_level with bound check;

tuned;

clarified signature: fewer tuples;