Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. try proof method "order" in Sledgehammer's proof reconstruction
  2. added Mirabelle action "order"
  3. renamed lemma antisymp_on_reflcp to antisymp_on_reflclp
  4. tuned proof
Changeset 80655:7793e3161d2b by desharna:
try proof method "order" in Sledgehammer's proof reconstruction
The file was addedsrc/HOL/Tools/Mirabelle/mirabelle_order.ML
The file was modified NEWS (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML (diff)
Changeset 80653:6a3212bedfad by desharna:
added Mirabelle action "order"
The file was modified NEWS (diff)
The file was modified src/HOL/Mirabelle.thy (diff)
Changeset 80652:5e85ea359563 by desharna:
renamed lemma antisymp_on_reflcp to antisymp_on_reflclp
The file was modified NEWS (diff)
The file was modified src/HOL/Transitive_Closure.thy (diff)
Changeset 80651:b045d20c9c3c by desharna:
tuned proof
The file was modified src/HOL/Transitive_Closure.thy (diff)