Summary
- more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
- integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
- added FIXMEs
The file was modified | src/HOL/Tools/ATP/atp_proof.ML (diff) |
The file was modified | src/HOL/Tools/ATP/atp_satallax.ML (diff) |
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) |
The file was modified | src/HOL/Library/Multiset_Order.thy (diff) |