Build #89 (Jan 30, 2022, 12:14:00 AM)

1. Added a tiny proof (detail)
2. Deletion of a duplicate proof (detail)
3. useful lemma integral_less (detail)
4. merged (detail)
5. removed unused parameter following f9908452b282 (detail)
6. treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis) (detail)
7. fixed dodgy intro! attributes (detail)
8. merged (detail)
9. optimized facts traversal in TPTP translation (detail)
10. optimized app_op_level selection in TPTP generation (detail)
11. tuned trivial check in mirabelle_sledgehammer (detail)
12. renamed run_action to run in Mirabelle.action record (detail)
13. added spying of fact filtering timing (detail)
14. tuned mirabelle_sledgehammer output (detail)
15. added spying to Sledgehammer (detail)
16. proper fact filter for dummy ATPs (detail)
17. added syping of fact filtering time to sledgehammer (detail)
18. removed unsynchronized references in mirabelle_sledgehammer (detail)
19. tuned mirabelle_sledgehammer to have a single call to Synchronized.change per run (detail)
20. updated to polyml-test-15c840d48c9a; (detail)

1. Cleanup. (detail)
2. Fewer parentheses around turnstile + remove unused lemmas. (detail)
3. Simplify proof of truth lemma. (detail)
4. Notation for `imply` and fewer parenthesis around turnstiles. (detail)
5. Abstract results to shorten proofs. (detail)
6. Better notation. (detail)
7. merged (detail)
8. tuned whitespace; (detail)
9. more symbols; (detail)
10. profer bundle lattice_syntax; (detail)
11. prefer existing lattice_syntax and no_lattice_syntax, with proper 'no_notation' as intended; (detail)
12. Add soundness and completeness for the PAL versions of systems K, T, KB, K4, S4 and S5. (detail)
13. avoid hardwired document output; (detail)
14. merged (detail)
15. deleting the overloading of div and mod, with its attendant ambiguities (detail)
16. replaced Erdős by Erd\H{o}s (fixed problem in LaTeX document generation) (detail)

Started by timer

This run spent:

• 0.14 sec waiting;
• 16 hr build duration;
• 16 hr total from scheduled to completion.