Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. avoid legacy binding errors in Sledgehammer Isar proofs
  2. parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition
  3. added argo
  4. allow (~) syntax in TPTP proofs for unapplied negation
  5. reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs
  6. use same associativity as Isabelle when parsing HOL proofs
  7. improved Sledgehammer's HOL proof parser w.r.t. negation
Changeset 78697:8ca71c0ae31f by blanchet:
avoid legacy binding errors in Sledgehammer Isar proofs
The file was modified src/HOL/Tools/ATP/atp_proof_reconstruct.ML (diff)
Changeset 78696:ef89f1beee95 by blanchet:
parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_proof_reconstruct.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML (diff)
Changeset 78695:41273636a82a by blanchet:
added argo
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML (diff)
Changeset 78694:5e995ceb7490 by blanchet:
allow (~) syntax in TPTP proofs for unapplied negation
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
Changeset 78693:1c0576840bf4 by blanchet:
reconstruct Zipperposition's if-then-else in Sledgehammer Isar proofs
The file was modified src/HOL/Tools/ATP/atp_proof_reconstruct.ML (diff)
Changeset 78692:1b0f5576f5e9 by blanchet:
use same associativity as Isabelle when parsing HOL proofs
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
Changeset 78691:1320782a394e by blanchet:
improved Sledgehammer's HOL proof parser w.r.t. negation
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)