equal
deleted
inserted
replaced
21 *} |
21 *} |
22 |
22 |
23 ML {* |
23 ML {* |
24 val do_it = false (* switch to "true" to generate the files *) |
24 val do_it = false (* switch to "true" to generate the files *) |
25 val params = Sledgehammer_Isar.default_params @{context} [] |
25 val params = Sledgehammer_Isar.default_params @{context} [] |
|
26 val prob_dir = "/tmp/mash_problems" |
26 *} |
27 *} |
27 |
28 |
28 ML {* |
29 ML {* |
29 if do_it then |
30 if do_it then |
30 evaluate_mash_suggestions @{context} params "/tmp/mash_suggestions" |
31 Isabelle_System.mkdir (Path.explode prob_dir) |
31 "/tmp/mash_eval.out" |
32 else |
|
33 () |
|
34 *} |
|
35 |
|
36 ML {* |
|
37 if do_it then |
|
38 evaluate_mash_suggestions @{context} params (SOME prob_dir) |
|
39 "/tmp/mash_suggestions" "/tmp/mash_eval.out" |
32 else |
40 else |
33 () |
41 () |
34 *} |
42 *} |
35 |
43 |
36 end |
44 end |