Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. NEWS
  2. merged
  3. used TH1 for Leo-III in sledgehammer
  4. tuned run_sledgehammer and called it directly from Mirabelle
  5. exported Sledgehammer.launch_prover and use it in Mirabelle
  6. proper filtering inf induction rules in Mirabelle
  7. added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle
  8. tuned ATP to use is_widely_irrelevant_const
  9. added support for initialization messages to Mirabelle
Changeset 74956:a7183a0a33e1 by desharna:
NEWS
The file was modified NEWS (diff)
Changeset 74955:6f5eafd952c9 by desharna:
merged
Changeset 74954:74c53a9027e2 by desharna:
used TH1 for Leo-III in sledgehammer
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
Changeset 74953:aade20a03edb by desharna:
tuned run_sledgehammer and called it directly from Mirabelle
The file was modified src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML (diff)
Changeset 74952:ae2185967e67 by desharna:
exported Sledgehammer.launch_prover and use it in Mirabelle
The file was modified src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
Changeset 74951:0b6f795d3b78 by desharna:
proper filtering inf induction rules in Mirabelle
The file was modified src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML (diff)
Changeset 74950:b350a1f2115d by desharna:
added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle
The file was modified src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML (diff)
Changeset 74949:90290869796f by desharna:
tuned ATP to use is_widely_irrelevant_const
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)
Changeset 74948:15ce207f69c8 by desharna:
added support for initialization messages to Mirabelle
The file was modified src/HOL/Mirabelle.thy (diff)
The file was modified src/HOL/Tools/Mirabelle/mirabelle.ML (diff)
The file was modified src/HOL/Tools/Mirabelle/mirabelle.scala (diff)
The file was modified src/HOL/Tools/Mirabelle/mirabelle_arith.ML (diff)
The file was modified src/HOL/Tools/Mirabelle/mirabelle_metis.ML (diff)
The file was modified src/HOL/Tools/Mirabelle/mirabelle_presburger.ML (diff)
The file was modified src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML (diff)
The file was modified src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML (diff)
The file was modified src/HOL/Tools/Mirabelle/mirabelle_try0.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML (diff)