tuned signature;

Thy_Header.read convenience;

some support for Session.File_Store;

tuned signature;

eliminated redundant session_ready;

tuned;

uniform finish_thy -- always Global_Theory.join_proofs, even with sequential scheduling;

misc tuning;

correction: do not assume that case const index covered all cases

remove illegal case combinators after merge

corrected misunderstanding what `old functions` are supposed to be

centralized deletion of equations for constructors; corrected misunderstanding what `old functions` are supposed to be

merged

index cases for constructors

cover induct's "arbitrary" more deeply

merged;

enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes

made minimizer informative output accurate

test a few more type encodings

further repair "mangled_tags", now that tags are also mangled

update documentation after "type_enc" renaming + fixed a few other out-of-date factlets

renamed "type_sys" to "type_enc", which is more accurate

document "simple_higher" type encoding

cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company

mangle "ti" tags

tuning

clarified Thy_Syntax.element;

tuned layout;

proper @{binding} antiquotations (relevant for formal references);

tuned;