Changes

Summary

1. merged
2. use strict Global_Theory.register_proofs as checkpoint for stored zproof, and thus reduce current zboxes;
3. clarified signature;
4. omit pointless future: proof terms are built sequentially;
5. omit unclear / inaccurate renaming;
6. more normalization: re-use Thm.solve_constraints as important checkpoint for results, notably Global_Theory.name_thm;
7. more robust: avoid assumption about Context.certificate_theory;
8. tuned;
9. clarified pro-forma proof: no zboxes here (partially revert 686b7b14d041);
10. tuned;
11. tuned;
12. more normalization;
13. less ambitious normalization: term abstractions over terms and proofs, but not proofs over proofs (which may be large);
14. tuned;
15. more thorough beta contraction, following Envir.norm_term;
16. tuned, following Envir.norm_term;
17. more operations;
18. merged
19. unused lemma
20. restore benchmark requirement heaps properly;
21. continue build while waiting for updated schedule;
22. clarified signature;
23. added start-up sequence for benchmark with requirements;
24. use single-threaded session build as benchmark (using ZF-Constructible);
25. separate build processes for scheduler and scheduled;
26. add delay and limit options for when schedule is considered outdated;
27. proper closing order;
28. read serial for schedules (amending 2039f360);