equal
deleted
inserted
replaced
|
1 (* Title: HOL/TPTP/MaSh_Eval.thy |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* MaSh Evaluation Driver *} |
|
6 |
|
7 theory MaSh_Eval |
|
8 imports Complex_Main |
|
9 uses "mash_eval.ML" |
|
10 begin |
|
11 |
|
12 sledgehammer_params |
|
13 [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, |
|
14 lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize] |
|
15 |
|
16 declare [[sledgehammer_instantiate_inducts]] |
|
17 |
|
18 ML {* |
|
19 open MaSh_Eval |
|
20 *} |
|
21 |
|
22 ML {* |
|
23 val do_it = false (* switch to "true" to generate the files *); |
|
24 val thy = @{theory List}; |
|
25 val params = Sledgehammer_Isar.default_params @{context} [] |
|
26 *} |
|
27 |
|
28 ML {* |
|
29 if do_it then |
|
30 evaluate_mash_suggestions @{context} params thy "/tmp/mash_suggestions_list" |
|
31 else |
|
32 () |
|
33 *} |
|
34 |
|
35 end |