Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
  2. integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
  3. added FIXMEs
Changeset 67022:49309fe530fd by blanchet:
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_satallax.ML (diff)
Changeset 67021:41f1f8c4259b by blanchet:
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
The file was modified src/Doc/manual.bib (diff)
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
Changeset 67020:c32254ab1901 by blanchet:
added FIXMEs
The file was modified src/HOL/Library/Multiset_Order.thy (diff)