use build_cluster in ci builds;

merged

tuned alias names in formulas

renamed theorems

add favicon to web app;

merged

clarified data representation: prefer explicit type Thm_Name;

more operations, following Isabelle/ML;

clarified signature: more explicit operations;

clarified treatment of Thm_Name.T (again, see also 8a9588ffc133);

clarified operations, including exceptions;

tuned: more direct Isabelle/ML;

clarified modules;

more accurate thm "name_hint", using Thm_Name.T;

more operationsd;

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;

tuned proof: avoid smt/z3 to make this work with arm64-linux;

proper afp_directory (amending 9308bc5f65d6);

clarified names;

clarified name: avoid clash with Library.Update;

clarified signature;