author | immler |
Sun, 27 Oct 2019 21:51:14 -0400 | |
changeset 71035 | 6fe5a0e1fa8e |
parent 69605 | a96320074298 |
child 73684 | a63d76ba0a03 |
permissions | -rw-r--r-- |
(* Title: HOL/Mirabelle/Mirabelle.thy Author: Jasmin Blanchette and Sascha Boehme, TU Munich *) theory Mirabelle imports Main begin ML_file \<open>Tools/mirabelle.ML\<close> ML_file \<open>../TPTP/sledgehammer_tactics.ML\<close> ML \<open>Toplevel.add_hook Mirabelle.step_hook\<close> ML \<open> signature MIRABELLE_ACTION = sig val invoke : (string * string) list -> theory -> theory end \<close> end