Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned mirabelle documentation
  2. removed support for obsolete prover SNARK and underperforming prover E-Par
  3. removed spurious documentation item
  4. removed obsolete unmaintained experimental prover Pirate
  5. tune filename
  6. drop obsolete ad hoc support for Satallax isar proof reconstruction
  7. recognize THF proofs properly
  8. factored out bit comprehension
  9. Fix formatting of default value in help message of "build_e" component.
Changeset 72404:31ddd23965e6 by blanchet:
tuned mirabelle documentation
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
Changeset 72403:4a3169d8885c by blanchet:
removed support for obsolete prover SNARK and underperforming prover E-Par
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
The file was modified src/HOL/Sledgehammer.thy (diff)
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
Changeset 72402:148e8332a8b1 by blanchet:
removed spurious documentation item
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
Changeset 72401:2783779b7dd3 by blanchet:
removed obsolete unmaintained experimental prover Pirate
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_atp_systems.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)
Changeset 72400:abfeed05c323 by desharna:
tune filename
The file was addedsrc/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
The file was modified src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML (diff)
The file was modified src/HOL/Sledgehammer.thy (diff)
The file was modified src/HOL/TPTP/atp_problem_import.ML (diff)
The file was modified src/HOL/TPTP/atp_theory_export.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_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_prover_smt.ML (diff)
The file was removedsrc/HOL/Tools/ATP/atp_systems.ML
Changeset 72399:f8900a5ad4a7 by desharna:
drop obsolete ad hoc support for Satallax isar proof reconstruction
The file was modified src/HOL/ATP.thy (diff)
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)
The file was removedsrc/HOL/Tools/ATP/atp_satallax.ML
Changeset 72398:5d1a7b688f6d by desharna:
recognize THF proofs properly
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_satallax.ML (diff)
Changeset 72397:48013583e8e6 by haftmann:
factored out bit comprehension
The file was modified src/HOL/Library/Bit_Operations.thy (diff)
The file was modified src/HOL/Word/Bit_Comprehension.thy (diff)
The file was modified src/HOL/Word/Misc_Typedef.thy (diff)
The file was modified src/HOL/Word/More_Word.thy (diff)
The file was modified src/HOL/Word/Word.thy (diff)
Changeset 72396:63e83aaec7a8 by desharna:
Fix formatting of default value in help message of "build_e" component.
The file was modified src/Pure/Admin/build_e.scala (diff)