Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tweaked Sledgehammer interaction
  2. there won't be an E version 2.7
  3. reverted 0506c3273814 -- the message is still useful
  4. compile
  5. adopt terminology suggested by Larry Paulson
  6. more robust E proof parsing
  7. avoid double 'Warning:' in Sledgehammer messages
  8. tweaked abduction in Sledgehammer
  9. slightly more documentation
  10. renamed new Sledgehammer option
  11. updated documentation
  12. improve ad hoc abduction in Sledgehammer
  13. tuning
  14. don't apply abduction and consistency checking to goals of the form 'False'
  15. implemented ad hoc abduction in Sledgehammer with E
Changeset 77432:e51aa922079a by blanchet:
tweaked Sledgehammer interaction
The file was modified src/HOL/Tools/ATP/atp_proof_reconstruct.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)
Changeset 77431:cdf5f392ea78 by blanchet:
there won't be an E version 2.7
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
Changeset 77430:51dac6fcdd0e by blanchet:
reverted 0506c3273814 -- the message is still useful
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_proof_reconstruct.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_util.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)
Changeset 77429:110988ad5b4c by blanchet:
compile
The file was modified src/HOL/TPTP/atp_theory_export.ML (diff)
Changeset 77428:7c76221baecb by blanchet:
adopt terminology suggested by Larry Paulson
The file was modified NEWS (diff)
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML (diff)
Changeset 77427:4cdefee3f97f by blanchet:
more robust E proof parsing
The file was modified src/HOL/Tools/ATP/atp_problem.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
Changeset 77426:4a6eb1b18340 by blanchet:
avoid double 'Warning:' in Sledgehammer messages
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
Changeset 77425:bde374587d93 by blanchet:
tweaked abduction in Sledgehammer
The file was modified src/Doc/Sledgehammer/document/root.tex (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)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)
Changeset 77424:73611eb994cf by blanchet:
slightly more documentation
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
Changeset 77423:779faa014564 by blanchet:
renamed new Sledgehammer option
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML (diff)
Changeset 77422:e10f15652026 by blanchet:
updated documentation
The file was modified NEWS (diff)
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
Changeset 77421:4e8a6354c54f by blanchet:
improve ad hoc abduction in Sledgehammer
The file was modified src/HOL/Tools/ATP/atp_proof_reconstruct.ML (diff)
Changeset 77420:f6cb40234009 by blanchet:
tuning
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
Changeset 77419:a15f0fcff041 by blanchet:
don't apply abduction and consistency checking to goals of the form 'False'
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
Changeset 77418:a8458f0df4ee by blanchet:
implemented ad hoc abduction in Sledgehammer with E
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_proof_reconstruct.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML (diff)