Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuning
  2. parse TPTP operator @ also when not parenthesized
  3. removed setup for outdated CVC3 from Isabelle
  4. tuned E's lambda encoding
  5. use Vampire's clausifier with iProver, now that E's is no longer supported
  6. updated Sledgehammer docs -- removed most version numbers since these are tedious to maintain
  7. compile
Changeset 74050:bed899f14df7 by blanchet:
tuning
The file was modified src/HOL/Tools/ATP/atp_proof_reconstruct.ML (diff)
Changeset 74049:d0b190b4f15d by blanchet:
parse TPTP operator @ also when not parenthesized
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
Changeset 74048:a0c9fc9c7dbe by blanchet:
removed setup for outdated CVC3 from Isabelle
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
The file was modified src/HOL/SMT.thy (diff)
The file was modified src/HOL/Tools/SMT/smt_systems.ML (diff)
Changeset 74047:a2b470e315ee by blanchet:
tuned E's lambda encoding
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
Changeset 74046:462d652ad910 by blanchet:
use Vampire's clausifier with iProver, now that E's is no longer supported
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
Changeset 74045:302994f5a3c2 by blanchet:
updated Sledgehammer docs -- removed most version numbers since these are tedious to maintain
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
Changeset 74044:943757b788f9 by blanchet:
compile
The file was modified src/HOL/TPTP/atp_theory_export.ML (diff)