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