equal
deleted
inserted
replaced
14 ML {* |
14 ML {* |
15 open MaSh_Import |
15 open MaSh_Import |
16 *} |
16 *} |
17 |
17 |
18 ML {* |
18 ML {* |
19 val do_it = true (* switch to "true" to generate the files *); |
19 val do_it = false (* switch to "true" to generate the files *); |
20 val thy = @{theory List} |
20 val thy = @{theory List}; |
|
21 val params = Sledgehammer_Isar.default_params @{context} [] |
21 *} |
22 *} |
22 |
23 |
23 ML {* |
24 ML {* |
24 if do_it then |
25 if do_it then |
25 import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions_list" |
26 import_and_evaluate_mash_suggestions @{context} params thy "/tmp/mash_suggestions_list" |
26 else |
27 else |
27 () |
28 () |
28 *} |
29 *} |
29 |
30 |
30 end |
31 end |