| changeset 73684 | a63d76ba0a03 |
| parent 69605 | a96320074298 |
| 73679:71c45d60a90a | 73684:a63d76ba0a03 |
|---|---|
5 theory Mirabelle |
5 theory Mirabelle |
6 imports Main |
6 imports Main |
7 begin |
7 begin |
8 |
8 |
9 ML_file \<open>Tools/mirabelle.ML\<close> |
9 ML_file \<open>Tools/mirabelle.ML\<close> |
10 ML_file \<open>../TPTP/sledgehammer_tactics.ML\<close> |
|
11 |
10 |
12 ML \<open>Toplevel.add_hook Mirabelle.step_hook\<close> |
11 ML \<open>Toplevel.add_hook Mirabelle.step_hook\<close> |
13 |
12 |
14 ML \<open> |
13 ML \<open> |
15 signature MIRABELLE_ACTION = |
14 signature MIRABELLE_ACTION = |