Skip to content
Success

Changes

Summary

  1. tuned Mirabelle
  2. merged
  3. refactored Mirabelle to produce output in real time
Changeset 73849:4eac16052a94 by desharna:
tuned Mirabelle
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_sledgehammer.ML (diff)
Changeset 73848:77306bf4e1ee by desharna:
merged
Changeset 73847:58f6b41efe88 by desharna:
refactored Mirabelle to produce output in real time
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_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/etc/options (diff)