Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. allow general command transactions with presentation;
  2. more operations;
  3. clarified signature;
  4. tuned signature;
  5. support Gradle as alternative to Maven (again);
  6. tuned mirabelle command-line help message
  7. updated Mirabelle documentation
  8. proper documentation for induction_rules Sledgehammer option
  9. NEWS
  10. merged
  11. used TH1 for Leo-III in sledgehammer
  12. tuned run_sledgehammer and called it directly from Mirabelle
  13. exported Sledgehammer.launch_prover and use it in Mirabelle
  14. proper filtering inf induction rules in Mirabelle
  15. added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle
  16. tuned ATP to use is_widely_irrelevant_const
  17. added support for initialization messages to Mirabelle
Changeset 74964:77a96ed74340 by wenzelm:
allow general command transactions with presentation;
The file was modified src/Pure/Isar/outer_syntax.ML
The file was modified src/Pure/Isar/toplevel.ML
Changeset 74963:29dfe75c058b by wenzelm:
more operations;
The file was modified src/Pure/General/json_api.scala
Changeset 74962:2c9c4ad4c816 by wenzelm:
clarified signature;
The file was modified src/Pure/General/json_api.scala
The file was modified src/Pure/Tools/flarum.scala
Changeset 74961:bb0858cc574e by wenzelm:
tuned signature;
The file was modified src/Pure/Tools/flarum.scala
Changeset 74960:f03ece7155d6 by wenzelm:
support Gradle as alternative to Maven (again);
The file was modified NEWS
The file was modified src/Doc/System/Scala.thy
The file was modified src/Pure/Tools/scala_project.scala
Changeset 74959:340c5f3506a8 by desharna:
tuned mirabelle command-line help message
The file was modified src/HOL/Tools/Mirabelle/mirabelle.scala
Changeset 74958:953f53f03437 by desharna:
updated Mirabelle documentation
The file was modified src/Doc/Sledgehammer/document/root.tex
Changeset 74957:089eeaaee525 by desharna:
proper documentation for induction_rules Sledgehammer option
The file was modified src/Doc/Sledgehammer/document/root.tex
Changeset 74956:a7183a0a33e1 by desharna:
NEWS
The file was modified NEWS
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
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
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
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
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML
Changeset 74951:0b6f795d3b78 by desharna:
proper filtering inf induction rules in Mirabelle
The file was modified src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
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
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
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
Changeset 74948:15ce207f69c8 by desharna:
added support for initialization messages to Mirabelle
The file was modified src/HOL/Mirabelle.thy
The file was modified src/HOL/Tools/Mirabelle/mirabelle.ML
The file was modified src/HOL/Tools/Mirabelle/mirabelle.scala
The file was modified src/HOL/Tools/Mirabelle/mirabelle_arith.ML
The file was modified src/HOL/Tools/Mirabelle/mirabelle_metis.ML
The file was modified src/HOL/Tools/Mirabelle/mirabelle_presburger.ML
The file was modified src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML
The file was modified src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
The file was modified src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML
The file was modified src/HOL/Tools/Mirabelle/mirabelle_try0.ML
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML

Summary

  1. adapted to new Sledgehammer.run_sledgehammer return type
Changeset 12324:e2ae9549a7b0 by desharna:
adapted to new Sledgehammer.run_sledgehammer return type
The file was modified thys/Proof_Strategy_Language/Subtool.ML