author | wenzelm |
Tue, 19 Jul 2016 09:55:03 +0200 | |
changeset 63520 | 2803d2b8f85d |
parent 63167 | 0909deb8059b |
child 69605 | a96320074298 |
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 \<open>Toplevel.add_hook Mirabelle.step_hook\<close> ML \<open> signature MIRABELLE_ACTION = sig val invoke : (string * string) list -> theory -> theory end \<close> end