equal
deleted
inserted
replaced
5 Evaluate proof suggestions from MaSh (Machine-learning for Sledgehammer). |
5 Evaluate proof suggestions from MaSh (Machine-learning for Sledgehammer). |
6 *) |
6 *) |
7 |
7 |
8 signature MASH_EVAL = |
8 signature MASH_EVAL = |
9 sig |
9 sig |
10 type params = Sledgehammer_Provers.params |
10 type params = Sledgehammer_Prover.params |
11 |
11 |
12 val MePoN : string |
12 val MePoN : string |
13 val MaSh_IsarN : string |
13 val MaSh_IsarN : string |
14 val MaSh_ProverN : string |
14 val MaSh_ProverN : string |
15 val MeSh_IsarN : string |
15 val MeSh_IsarN : string |
26 |
26 |
27 open Sledgehammer_Util |
27 open Sledgehammer_Util |
28 open Sledgehammer_Fact |
28 open Sledgehammer_Fact |
29 open Sledgehammer_MePo |
29 open Sledgehammer_MePo |
30 open Sledgehammer_MaSh |
30 open Sledgehammer_MaSh |
31 open Sledgehammer_Provers |
31 open Sledgehammer_Prover |
32 open Sledgehammer_Commands |
32 open Sledgehammer_Commands |
33 |
33 |
34 val prefix = Library.prefix |
34 val prefix = Library.prefix |
35 |
35 |
36 val MaSh_IsarN = MaShN ^ "-Isar" |
36 val MaSh_IsarN = MaShN ^ "-Isar" |