#1845 (Dec 24, 2022, 12:50:10 AM)

1. tuned signature; (detail / hgweb)
2. tuned signature; (detail / hgweb)
3. more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
   prefer global operations for snapshot() and rendering(); (detail / hgweb)
4. update URL; (detail / hgweb)
5. clarified signature; (detail / hgweb)
6. tuned; (detail / hgweb)
7. tuned; (detail / hgweb)
8. tuned; (detail / hgweb)
9. tuned; (detail / hgweb)
10. tuned; (detail / hgweb)
11. clarified signature: more explicit types; (detail / hgweb)
12. merged (detail / hgweb)
13. merged (detail / hgweb)
14. used transp_on in assumptions of lemmas Multiset.bex_(least|greatest)_element (detail / hgweb)
15. added lemma trans_on_lex_prod[simp] (detail / hgweb)
16. strengthened and renamed lemma trans_converse and added lemma transp_on_conversep (detail / hgweb)
17. strengthened and renamed trans_reflclI (detail / hgweb)
18. strengthened and renamed transp_reflclp (detail / hgweb)
19. strengthened and renamed lemmas preorder.transp_(ge|gr|le|less) (detail / hgweb)
20. added lemmas trans_on_subset and transp_on_subset (detail / hgweb)
21. added lemmas trans_onD and transp_onD (detail / hgweb)
22. added lemmas trans_onI and transp_onI (detail / hgweb)
23. added lemma transp_on_trans_on_eq[pred_set_conv] (detail / hgweb)
24. fixed code-generation failure (detail / hgweb)
25. added predicates trans_on and transp_on and redefined trans and transp to be abbreviations (detail / hgweb)

Started by an SCM change

This run spent:

• 8.7 sec waiting;
• 1 hr 51 min build duration;
• 1 hr 51 min total from scheduled to completion.