more robust: avoid assumption about Context.certificate_theory;

tuned;

clarified pro-forma proof: no zboxes here (partially revert 686b7b14d041);

tuned;

tuned;

more normalization;

less ambitious normalization: term abstractions over terms and proofs, but not proofs over proofs (which may be large);

tuned;

more thorough beta contraction, following Envir.norm_term;

tuned, following Envir.norm_term;

more operations;

merged

unused lemma

restore benchmark requirement heaps properly;

continue build while waiting for updated schedule;

clarified signature;

added start-up sequence for benchmark with requirements;

use single-threaded session build as benchmark (using ZF-Constructible);

separate build processes for scheduler and scheduled;

add delay and limit options for when schedule is considered outdated;

proper closing order;

read serial for schedules (amending 2039f360);

more thorough beta contraction; removed unused operations;

tuned whitespace;

tuned;

more operations, following proofterm.ML;

tuned;

clarified signature, following Term.subst_bounds_same;

tuned whitespace;

minor performance tuning: more concise union;

tuned comments;

tuned, following close_proof;

proper treatment of proof hyps, following 8368160d3c65;

proper treatment of proof hyps: unchangeable, like bound;

proper Thm.transfer (required for zproofs);

clarified signature;

proper beta_norm after instantiation (amending 90c5aadcc4b2);

minor performance tuning: more direct beta_norm;

more robust norm_proof: turn env into instantiation, based on visible statement;

proper scope of cache (amending 61af3e917597);

tuned comments;

tuned names;

tuned signature;

more zproofs;

more operations: zterm ordering that follows fast_term_ord;

clarified signature; clarified modules;

clarified modules;

more zproofs;

more zproofs, imitating existing proofs (which are a bit rough here);

tuned signature;

tuned whitespace;

minor performance tuning;

tuned comments (see also 476a239d3e0e and possibly 4b62e0cb3aa8);

merged

minor performance tuning;

tuned;

minor performance tuning: prefer Same.operation;

clarified signature; minor performance tuning: avoid redundant identity;

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;

clarified signature: fewer tuples;

clarified signature: more explicit get_proofs_level with bounds check;

merged

misc tuning and clarification: more standard Same.commit discipline;

tuned;

tuned names;

more operations; more accurate treatment of beta contraction in norm_term/norm_proof, following Envir.norm_term;

minor performance tuning: more careful treatment of empty environment;

clarified signature;

more zproofs;

clarified signature: support shared cache;

tuned;

tuned: avoid shadowing;

more zproofs;

tuned;

more operations; clarified cache;

tuned signature;

tuned names;

tuned -- eliminate clones;

tuned;

more operations;

more operations;

tuned;

clarified signature;

tuned;

tuned;

consider schedule calculation time in estimation;

compare previous build schedule with new one, to prevent regressions;

clarified: build schedules may be outdated when empty, after some time, or due to build progress;

store previous build jobs in graph so schedules can be used later in the build process;

add serial for build schedule to avoid unnecessary db read/writes;

tuned;