tuned;

more robust: prefer synchronous compression (usually <= 1ms, sometimes 1..5ms);

clarified signature;

clarified output, following Consumer_Thread.failure;

more informative exception output, with optional trace;

more accurate output of Thm_Name.T wrt. facts name space;

clarified signature: more operations;

tuned structure;

tuned;

more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;

clarified signature: prefer explicit operation;

clarified signature;

tuned: prefer Thm_Name operations;

tuned;

prefer dynamic position from command transaction;

tuned signature;

clarified signature: more explicit preprocessing;

clarified signature: separate formal context from exported theory_name;

tuned signature: just one ZThm is sufficient;

renamed lemmas

build manager: echo error messages to server output;

omit showing previous failures for user builds;

always handle interrupted jobs;

add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;

clarified context: operations now in build process;

clarified: add explicit build process;

remove unnecessary subdir;

tuned;