#1841 (Dec 20, 2022, 12:50:10 AM)

1. merged (detail / hgweb)
2. added lemma refl_lex_prod[simp] (detail / hgweb)
3. added lemmas reflI and reflD (detail / hgweb)
4. added lemmas asym_on_lex_prod[simp] and asym_lex_prod[simp] (detail / hgweb)
5. added lemmas sym_on_lex_prod[simp] and sym_lex_prod[simp] (detail / hgweb)
6. added lemmas irrefl_on_lex_prod[simp] and irrefl_lex_prod[simp] (detail / hgweb)
7. strengthened and renamed lemmas asym_if_irrefl_and_trans and asymp_if_irreflp_and_transp (detail / hgweb)
8. strengthened and renamed lemma antisym_converse and added lemma antisymp_on_conversep (detail / hgweb)
9. added lemmas asym_on_converse[simp] and asymp_on_conversep[simp] (detail / hgweb)
10. strengthened and renamed lemma sym_converse and added lemma symp_on_conversep (detail / hgweb)
11. strengthened and renamed lemmas antisymp_less and antisymp_greater (detail / hgweb)
12. strengthened lemmas antisym_on_if_asym_on and antisymp_on_if_asymp_on (detail / hgweb)
13. tuned naming (detail / hgweb)
14. added lemma asymp_on_asym_on_eq[pred_set_conv] (detail / hgweb)
15. strengthened and renamed asymp_less and asymp_greater (detail / hgweb)
16. added lemmas asym_on_subset and asymp_on_subset (detail / hgweb)
17. added lemmas asym_onI, asymp_onI, asym_onD, and asymp_onD (detail / hgweb)
18. added predicates asym_on and asymp_on and redefined asym and asymp to be abbreviations (detail / hgweb)

Started by an SCM change

This run spent:

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