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)

more uniform instT_subst vs. inst_subst: compare variable names only;

tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;

misc tuning and modernization;

some performance tuning via Term_Subst/Same.operation; tuned;

pruned signature;

added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types; tuned;

more conventional syntax const;

proper syntactic category for abstraction syntax, to avoid low-level exception for malformed "\<integral> x y. f \<partial>M", for example;

merged

prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);

document new experimental provers

added remote iProver(-Eq) for experimentation