timing function generation bug fix by Jonas Stahl

tuned signature: more types, fewer warnings in IntelliJ IDEA;

new less ad hoc implementation of the 'moura' tactic for skolemization

more thorough Store.clean_output (amending 1fa1b32b0379);

clarified signature: Build_Process tells how to clean sessions;

clarified signature;

tuned;

tuned;

minor performance tuning;

tuned;

tuned signature;

tuned, following 7a1153c95bf9;

merged

tuned signature: fewer warnings in IntelliJ IDEA;

proper usage;

recover "build_database_server" from 1fa1b32b0379: still required, e.g. in build_benchmark;

clarified signature;

more robust: make double-sure that heap digest is present;

tuned;

minor performance tuning: just one transaction for log_db without heap;

tuned;

proper store.cache.compress;

tuned whitespace;

clarified store_session: heap requires process_result.ok, but log_db is always stored; clarified ML_Heap.clean_entry vs. ML_Heap.init_entry;