changeset 63167 | 0909deb8059b |
parent 59574 | de392405a851 |
child 69605 | a96320074298 |
--- a/src/HOL/Mirabelle/Mirabelle.thy Thu May 26 16:57:14 2016 +0200 +++ b/src/HOL/Mirabelle/Mirabelle.thy Thu May 26 17:51:22 2016 +0200 @@ -9,13 +9,13 @@ ML_file "Tools/mirabelle.ML" ML_file "../TPTP/sledgehammer_tactics.ML" -ML {* Toplevel.add_hook Mirabelle.step_hook *} +ML \<open>Toplevel.add_hook Mirabelle.step_hook\<close> -ML {* +ML \<open> signature MIRABELLE_ACTION = sig val invoke : (string * string) list -> theory -> theory end -*} +\<close> end