Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. more Mailman archives;
  3. more Mailman content;
  4. clarified signature;
  5. tuned metis to use map_index
  6. merged
  7. fixed HOL-TPTP
  8. tuned vars_of_iterm
  9. fixed TPTP generation of multi-arity expressions
  10. proper handling of Hilbert choice in TFX logics
  11. proper tptp_builtins
  12. reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
  13. proper proxy for Hilbert choice in TPTP output
  14. proper polymorphism for TH1 format in Sledgehammer
  15. refactored $ite and $let configuration and added dummy_thf_reduced prover
  16. tuned TPTP file names generated by Sledgehammer
  17. tuned SMT-Lib file names generated by Mirabelle
  18. added support for higher-order SMT proof search in Sledgehammer
  19. separated FOOL from $ite/$let in TPTP output
Changeset 74908:7423bfe7c038 by wenzelm:
merged
Changeset 74907:af2323593473 by wenzelm:
more Mailman archives;
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
The file was modified src/Pure/General/mailman.scala (diff)
Changeset 74906:9702913db56c by wenzelm:
more Mailman content;
The file was modified src/Pure/General/mailman.scala (diff)
Changeset 74905:246e22068141 by wenzelm:
clarified signature;
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
The file was modified src/Pure/General/mailman.scala (diff)
Changeset 74904:cab76af373e7 by desharna:
tuned metis to use map_index
The file was modified src/HOL/Tools/Metis/metis_generate.ML (diff)
The file was modified src/HOL/Tools/Metis/metis_reconstruct.ML (diff)
The file was modified src/HOL/Tools/Metis/metis_tactic.ML (diff)
Changeset 74903:d969474ddc45 by desharna:
merged
Changeset 74902:ece4f07ebb04 by desharna:
fixed HOL-TPTP
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 74901:2cbb5f6a854f by desharna:
tuned vars_of_iterm
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)
Changeset 74900:21ea15129166 by desharna:
fixed TPTP generation of multi-arity expressions
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)
Changeset 74899:b4beb55c574e by desharna:
proper handling of Hilbert choice in TFX logics
The file was modified src/HOL/ATP.thy (diff)
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)
Changeset 74898:e83224066f19 by desharna:
proper tptp_builtins
The file was modified src/HOL/Tools/ATP/atp_problem.ML (diff)
Changeset 74897:8b1ab558e3ee by desharna:
reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
The file was modified src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML (diff)
Changeset 74896:f9908452b282 by desharna:
proper proxy for Hilbert choice in TPTP output
The file was modified src/HOL/ATP.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)
Changeset 74895:b605ebd87a47 by desharna:
proper polymorphism for TH1 format in Sledgehammer
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
Changeset 74894:a64a8f7d593e by desharna:
refactored $ite and $let configuration and added dummy_thf_reduced prover
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
Changeset 74893:dacd9a08f0a3 by desharna:
tuned TPTP file names generated by Sledgehammer
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)
Changeset 74892:3094dae03764 by desharna:
tuned SMT-Lib file names generated by Mirabelle
The file was modified src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML (diff)
Changeset 74891:db4b8dd587a5 by desharna:
added support for higher-order SMT proof search in Sledgehammer
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML (diff)
Changeset 74890:11e34ffc65e4 by desharna:
separated FOOL from $ite/$let in TPTP output
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/Sledgehammer/sledgehammer_atp_systems.ML (diff)