#1709 (Jun 9, 2022, 1:34:05 AM)

1. proper make_port for regular situation;
   tuned whitespace; (detail / hgweb)
2. clarified types -- proper default_port via make_port; (detail / hgweb)
3. proper nominal_port, notably for port forwarding; (detail / hgweb)
4. some additional lemmas and a little tidying up (detail / hgweb)
5. merged (detail / hgweb)
6. added lemma totalp_on_total_on_eq[pred_set_conv] (detail / hgweb)
7. added lemma reflp_on_empty[simp] and totalp_on_empty[simp] (detail / hgweb)
8. removed non-standard spaces in output (detail / hgweb)

Started by an SCM change

This run spent:

• 44 min waiting;
• 1 hr 36 min build duration;
• 2 hr 21 min total from scheduled to completion.