Summary
- 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) |
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) |