proof boxes based on proof digest (not proof term): thus it works with prune_proofs;

proper Thm.transfer;

clarified files;

clarified proof_boxes (requires prune_proofs=false);

tuned;

more robust;

more robust: avoid looping Lazy.force due to misinterpreted interrupt;

more informative combination_proof, e.g. relevant for proper type inference in HOL.Product_Type (with export_proofs);

tuned -- more stable type inference;

updated to jdk-11.0.4+11;

updated to scala-2.12.10;

more support for proof terms; clarified signature;

more support for proof terms;

support for proof terms;

clarified proof export;

set_preproc for object-logics with type classes;

tuned signature;

skip (somewhat pointless) shrink_proof more uniformly;

apply_preproc for all proof boxes;

cumulative errors for session partitions;

proper guard for process_theory: ensure uniform precedence of results;

load HOL-Proofs first: it introduces some extra "thm" items that are required later on;

clarified count_file;

clarified modules;

more complete coverage of sessions: process_theory operation needs to handle duplicate theories;

proper build_graph to make session selection work as in "isabelle build";

incorporate sessions with record_proofs;

clarified options;

clarified signature;

clarified signature;