equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* MaSh Evaluation Driver *} |
5 header {* MaSh Evaluation Driver *} |
6 |
6 |
7 theory MaSh_Eval |
7 theory MaSh_Eval |
8 imports (* ### Complex_Main *) "~~/src/HOL/Sledgehammer2d" |
8 imports Complex_Main |
9 uses "mash_eval.ML" |
9 uses "mash_eval.ML" |
10 begin |
10 begin |
11 |
11 |
12 sledgehammer_params |
12 sledgehammer_params |
13 [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, |
13 [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, |
18 ML {* |
18 ML {* |
19 open MaSh_Eval |
19 open MaSh_Eval |
20 *} |
20 *} |
21 |
21 |
22 ML {* |
22 ML {* |
23 val do_it = false (* switch to "true" to generate the files *); |
23 val do_it = false (* switch to "true" to generate the files *) |
24 val thy = @{theory Nat}; |
24 val thy = @{theory Nat} |
25 val params = Sledgehammer_Isar.default_params @{context} [] |
25 val params = Sledgehammer_Isar.default_params @{context} [] |
26 *} |
26 *} |
27 |
27 |
28 ML {* |
28 ML {* |
29 if do_it then |
29 if do_it then |
30 evaluate_mash_suggestions @{context} params thy "/Users/blanchet/tum/mash/mash/results/natNB200ATP-15.pred" |
30 evaluate_mash_suggestions @{context} params thy "/tmp/mash_suggestions" |
31 else |
31 else |
32 () |
32 () |
33 *} |
33 *} |
34 |
34 |
35 end |
35 end |