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