merged

cascading timeouts in minimizer, part 2

tuning

use "Time.time" rather than milliseconds internally

tune: no need for option

cascading timeouts in minimizer

shortcut binary minimization algorithm

speed up binary minimizer in practice by preferring the first half of the used facts (which are likelier to be relevant) to the second half

renamed experimental systems

repaired quantification over type variables for non-TFF1/THF encodings

misc tuning and modernization; more antiquotations;

misc tuning and modernization; more antiquotations;

tuned;

some statespace benchmarks;

write changed .prv files only, to avoid writing into src file-space by default;

tuned document; tuned proofs;

more precise dependencies;

inlined antiquotations;

misc tuning and modernization;

optional timing, to avoid redundant allocation of mutable cells;

tuned;

misc tuning;

merged

more use of global operations (see 98ec8b51af9c)