Changes

Summary

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