Build #74 (Oct 17, 2021, 12:14:00 AM)

1. A few new lemmas plus some refinements (detail)
2. merged (detail)
3. produced Mirabelle output directly in ML until Scala output gets fixed (detail)
4. clarified signature; (detail)
5. clarified signature; (detail)
6. clarified signature; (detail)
7. removed unused material (left-over from fd0c85d7da38); (detail)
8. support HOL-Isar_Examples.Hoare as well (amending 403ce50e6a2a); (detail)
9. removed junk; (detail)
10. merged (detail)
11. separated commands from annotations to be able to abstract about the latter only (detail)
12. prefer standard Term.dest_abs, with minor deviation of generated names; (detail)
13. tuned comments; (detail)
14. more examples (detail)
15. workaround for old macOS versions, after change of Let's Encrypt root certificate --- see also https://letsencrypt.org/docs/dst-root-ca-x3-expiration-september-2021 --- Java/Scala Isabelle_System.download() works, but curl doens't; (detail)
16. more complete simp rules (detail)
17. more complete simp rules (detail)
18. avoid overaggressive contraction of conversions (detail)
19. normalizing NOT (numeral _) (again) (detail)

1. Simplified a definition (detail)
2. modify propa (detail)
3. bit singleton shifts recovered for the sake of backward compatibility (detail)
4. updated to 7422950f3955 (detail)
5. merge (detail)
6. EPO: simplify proof (detail)
7. primer (detail)
8. more complete simp rules (detail)
9. more complete simp rules (examples) (detail)
10. avoid overaggressive contraction of conversions (detail)
11. slightly more prominence for proof tools; more examples (detail)

Started by timer

This run spent:

• 28 ms waiting;
• 18 hr build duration;
• 18 hr total from scheduled to completion.