author | Manuel Eberl <eberlm@in.tum.de> |
Tue, 19 Jan 2016 11:19:25 +0100 | |
changeset 62201 | eca7b38c8ee5 |
parent 59574 | de392405a851 |
child 63167 | 0909deb8059b |
permissions | -rw-r--r-- |
(* Title: HOL/Mirabelle/Mirabelle.thy Author: Jasmin Blanchette and Sascha Boehme, TU Munich *) theory Mirabelle imports Main begin ML_file "Tools/mirabelle.ML" ML_file "../TPTP/sledgehammer_tactics.ML" ML {* Toplevel.add_hook Mirabelle.step_hook *} ML {* signature MIRABELLE_ACTION = sig val invoke : (string * string) list -> theory -> theory end *} end