Session HOL-Mirabelle

Theories

• Mirabelle
  • File ‹Tools/mirabelle.ML›
  • File ‹~~/src/HOL/TPTP/sledgehammer_tactics.ML›
• Mirabelle_Test
  • File ‹Tools/mirabelle_arith.ML›
  • File ‹Tools/mirabelle_metis.ML›
  • File ‹Tools/mirabelle_quickcheck.ML›
  • File ‹Tools/mirabelle_refute.ML›
  • File ‹Tools/mirabelle_sledgehammer.ML›
  • File ‹Tools/mirabelle_sledgehammer_filter.ML›
  • File ‹Tools/mirabelle_try0.ML›