#461 (Oct 31, 2017, 12:50:09 AM)

1. added 'mlex_iff' lemma and simplified proof (detail / hgweb)
2. merged (detail / hgweb)
3. recovered document from 9bfb6978eb80; (detail / hgweb)
4. NEWS; (detail / hgweb)
5. obsolete; (detail / hgweb)
6. tuned; (detail / hgweb)
7. ROOT cleanup: empty 'document_files' means there is no document; (detail / hgweb)
8. eliminated pointless warning (see a35af478aee4): empty 'document_files' means there is no document; (detail / hgweb)
9. more informative timeout message, notably for build_status; (detail / hgweb)
10. clarified: adapted to ML version; (detail / hgweb)
11. proper order of initialization (amending 9953ae603a23); (detail / hgweb)
12. More topological results overlooked last time (detail / hgweb)
13. merged (detail / hgweb)
14. New results in topology, mostly from HOL Light's moretop.ml (detail / hgweb)
15. generalized some lemmas on multisets (detail / hgweb)
16. rule out pathologic instances (detail / hgweb)
17. tuned some proofs and added some lemmas (detail / hgweb)

Started by an SCM change

This run spent:

• 7 sec waiting;
• 1 hr 31 min build duration;
• 1 hr 31 min total from scheduled to completion.