1(* Title: HOL/Mirabelle/Mirabelle.thy 2 Author: Jasmin Blanchette and Sascha Boehme, TU Munich 3*) 4 5theory Mirabelle 6imports Main 7begin 8 9ML_file \<open>Tools/mirabelle.ML\<close> 10ML_file \<open>../TPTP/sledgehammer_tactics.ML\<close> 11 12ML \<open>Toplevel.add_hook Mirabelle.step_hook\<close> 13 14ML \<open> 15signature MIRABELLE_ACTION = 16sig 17 val invoke : (string * string) list -> theory -> theory 18end 19\<close> 20 21end 22