Changes

Summary

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

Summary

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