equal
deleted
inserted
replaced
21 ML \<open> |
21 ML \<open> |
22 open MaSh_Eval |
22 open MaSh_Eval |
23 \<close> |
23 \<close> |
24 |
24 |
25 ML \<open> |
25 ML \<open> |
26 val params = Sledgehammer_Commands.default_params @{theory} [] |
26 val params = Sledgehammer_Commands.default_params \<^theory> [] |
27 val prob_dir = prefix ^ "mash_problems" |
27 val prob_dir = prefix ^ "mash_problems" |
28 \<close> |
28 \<close> |
29 |
29 |
30 ML \<open> |
30 ML \<open> |
31 if do_it then |
31 if do_it then |
34 () |
34 () |
35 \<close> |
35 \<close> |
36 |
36 |
37 ML \<open> |
37 ML \<open> |
38 if do_it then |
38 if do_it then |
39 evaluate_mash_suggestions @{context} params range (SOME prob_dir) |
39 evaluate_mash_suggestions \<^context> params range (SOME prob_dir) |
40 [prefix ^ "mepo_suggestions", |
40 [prefix ^ "mepo_suggestions", |
41 prefix ^ "mash_suggestions", |
41 prefix ^ "mash_suggestions", |
42 prefix ^ "mash_prover_suggestions", |
42 prefix ^ "mash_prover_suggestions", |
43 prefix ^ "mesh_suggestions", |
43 prefix ^ "mesh_suggestions", |
44 prefix ^ "mesh_prover_suggestions"] |
44 prefix ^ "mesh_prover_suggestions"] |