#1001 (Mar 20, 2024, 9:15:10 PM)

1. added lemma wellorder.wfp_on_less[simp] (detail / hgweb)
2. merged (detail / hgweb)
3. HOL-Library: added modulo/congruence for real numbers (detail / hgweb)
4. only print schedule if relevant; (detail / hgweb)
5. remove laziness: no need, and errors during initialization loop with close(); (detail / hgweb)
6. more general definition of meromorphicity; Weierstraß factorisation theorem (detail / hgweb)
7. always provide build_database_server option in benchmark command; (detail / hgweb)
8. always check if node is defined, e.g. for exists_next operation wit empty schedule; (detail / hgweb)

Started by an SCM change

This run spent:

• 8 sec waiting;
• 5 hr 5 min build duration;
• 5 hr 5 min total from scheduled to completion.