Summary
- use simplifier to classify the missing assumptions in Sledgehammer's abduction mechanism
- don't try to falisfy goals with schematics
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) |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff) |