equal
deleted
inserted
replaced
4 |
4 |
5 theory Mirabelle |
5 theory Mirabelle |
6 imports Main |
6 imports Main |
7 begin |
7 begin |
8 |
8 |
9 ML_file "Tools/mirabelle.ML" |
9 ML_file \<open>Tools/mirabelle.ML\<close> |
10 ML_file "../TPTP/sledgehammer_tactics.ML" |
10 ML_file \<open>../TPTP/sledgehammer_tactics.ML\<close> |
11 |
11 |
12 ML \<open>Toplevel.add_hook Mirabelle.step_hook\<close> |
12 ML \<open>Toplevel.add_hook Mirabelle.step_hook\<close> |
13 |
13 |
14 ML \<open> |
14 ML \<open> |
15 signature MIRABELLE_ACTION = |
15 signature MIRABELLE_ACTION = |