more precise iterate_entries_after if start refers to last entry; do not assign exec states after bad theory init; reject illegal theory header after end of theory;

clarified define_command: store name as structural information;

amended last_common, if that happens to the very last entry (important to load HOL/Auth, for example); clarified touch_node: reset result explicitly;

more redable Document.Node.toString;

sort wrt. theory name;

modernized theory name;

repaired benchmarks;

merged

tuning

always measure time for ATPs -- auto minimization relies on it