Skip to content
Success

Changes

Summary

  1. deal with new-style Vampire skolemization in reconstructed Isar proofs
Changeset 79730:4031aafc2dda by blanchet:
deal with new-style Vampire skolemization in reconstructed Isar proofs
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)