Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Removed development code wrongfully committed
  2. Tuned documentation
  3. Updated ML in forgotten in previous commit
  4. Merged
  5. Expanded and tuned documentation
  6. Added support for TFX to Sledgehammer
  7. merged
  8. tuned
  9. Tuned indentation
  10. Tuned isar_step datatype
  11. Tuned isar_proofs constructions
  12. Tuned isar_proof datatype
  13. bundled syntax for state monad combinators
Changeset 72593:914f1f98839c by desharna:
Removed development code wrongfully committed
The file was modified src/HOL/ATP.thy (diff)
The file was modified src/HOL/Sledgehammer.thy (diff)
Changeset 72592:b6b6248d4719 by desharna:
Tuned documentation
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
The file was modified src/Doc/manual.bib (diff)
Changeset 72591:56514a42eee8 by desharna:
Updated ML in forgotten in previous commit
The file was modified src/HOL/TPTP/ATP_Theory_Export.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)
Changeset 72590:7b7227d9ae5e by desharna:
Merged
Changeset 72589:20587c17cb20 by desharna:
Expanded and tuned documentation
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
Changeset 72588:c7e2a9bdc585 by desharna:
Added support for TFX to Sledgehammer
The file was addedsrc/HOL/Tools/ATP/scripts/dummy_atp
The file was modified src/HOL/ATP.thy (diff)
The file was modified src/HOL/Sledgehammer.thy (diff)
The file was modified src/HOL/Tools/ATP/atp_problem.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (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 72587:f5507622baa9 by nipkow:
merged
Changeset 72586:e3ba2578ad9d by nipkow:
tuned
The file was modified src/HOL/Data_Structures/Interval_Tree.thy (diff)
The file was modified src/HOL/Data_Structures/RBT_Set.thy (diff)
The file was modified src/HOL/Data_Structures/Tree2.thy (diff)
The file was modified src/HOL/Data_Structures/Tree23.thy (diff)
The file was modified src/HOL/Library/Tree.thy (diff)
Changeset 72585:18eb7ec2720f by desharna:
Tuned indentation
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)
Changeset 72584:4ea19e5dc67e by desharna:
Tuned isar_step datatype
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML (diff)
Changeset 72583:e728d3a3d383 by desharna:
Tuned isar_proofs constructions
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML (diff)
Changeset 72582:b69a3a7655f2 by desharna:
Tuned isar_proof datatype
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML (diff)
Changeset 72581:de581f98a3a1 by haftmann:
bundled syntax for state monad combinators
The file was modified NEWS (diff)
The file was modified src/HOL/Library/DAList.thy (diff)
The file was modified src/HOL/Library/FSet.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/Open_State_Syntax.thy (diff)
The file was modified src/HOL/Probability/PMF_Impl.thy (diff)
The file was modified src/HOL/Product_Type.thy (diff)
The file was modified src/HOL/Quickcheck_Random.thy (diff)
The file was modified src/HOL/Random.thy (diff)
The file was modified src/HOL/Rat.thy (diff)
The file was modified src/HOL/Real.thy (diff)