#1922 (Mar 23, 2023, 12:50:09 AM)

1. reordered assumption and tuned proof of Multiset.bex_least_element and Multiset.bex_greatest_element (detail / hgweb)
2. added lemmas Finite_Set.bex_least_element and Finite_Set.bex_greatest_element (detail / hgweb)
3. refactored proofs (detail / hgweb)
4. added lemmas Finite_Set.bex_min_element and Finite_Set.bex_max_element (detail / hgweb)
5. reversed import dependency between Relation and Finite_Set; and move theorems around (detail / hgweb)

Started by an SCM change

This run spent:

• 7.8 sec waiting;
• 1 hr 52 min build duration;
• 1 hr 52 min total from scheduled to completion.