Mon, 25 Sep 2023 17:16:32 +0200 | blanchet | parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition | changeset | files |
Mon, 25 Sep 2023 17:16:32 +0200 | blanchet | added argo | changeset | files |
Mon, 25 Sep 2023 17:16:32 +0200 | blanchet | allow (~) syntax in TPTP proofs for unapplied negation | changeset | files |
Mon, 25 Sep 2023 17:16:32 +0200 | blanchet | reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs | changeset | files |
Mon, 25 Sep 2023 17:16:32 +0200 | blanchet | use same associativity as Isabelle when parsing HOL proofs | changeset | files |
Mon, 25 Sep 2023 17:16:32 +0200 | blanchet | improved Sledgehammer's HOL proof parser w.r.t. negation | changeset | files |