Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. use simplifier to classify the missing assumptions in Sledgehammer's abduction mechanism
  2. don't try to falisfy goals with schematics
Changeset 77602:7c25451ae2c1 by blanchet:
use simplifier to classify the missing assumptions in Sledgehammer's abduction mechanism
The file was modified src/HOL/Sledgehammer.thy (diff)
The file was modified src/HOL/Tools/ATP/atp_proof_reconstruct.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)
Changeset 77601:d39027e1c8c5 by blanchet:
don't try to falisfy goals with schematics
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)