proper sequential version;

eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer); clarified Command.run_process etc.: join running eval, bypass running print; eliminated Command.memo in favour of regular Lazy.lazy; more Lazy.lazy status information;

modernized historic example;

more thorough Lazy.is_finished;

3 old example lemmas by Amine listed in the top 100 theorems

update_cartouches; trimmed whitespace;

memo_fork without locking, to avoid rare deadlock in Event_Timer.request due to execution overrun;

typos

unused;

tuned message;