#2022 (Sep 26, 2023, 12:50:09 AM)

1. avoid legacy binding errors in Sledgehammer Isar proofs (detail / hgweb)
2. parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition (detail / hgweb)
3. added argo (detail / hgweb)
4. allow (~) syntax in TPTP proofs for unapplied negation (detail / hgweb)
5. reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs (detail / hgweb)
6. use same associativity as Isabelle when parsing HOL proofs (detail / hgweb)
7. improved Sledgehammer's HOL proof parser w.r.t. negation (detail / hgweb)

Started by an SCM change

This run spent:

• 7.9 sec waiting;
• 2 hr 2 min build duration;
• 2 hr 2 min total from scheduled to completion.