equal
deleted
inserted
replaced
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??, |
14 lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize] |
14 lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize] |
15 |
15 |
16 ML {* |
16 ML {* |
17 open Sledgehammer_Filter_MaSh |
|
18 open MaSh_Export |
17 open MaSh_Export |
19 *} |
18 *} |
20 |
19 |
21 ML {* |
20 ML {* |
22 val do_it = false (* switch to "true" to generate the files *); |
21 val do_it = false (* switch to "true" to generate the files *); |
24 val params = Sledgehammer_Isar.default_params @{context} [] |
23 val params = Sledgehammer_Isar.default_params @{context} [] |
25 *} |
24 *} |
26 |
25 |
27 ML {* |
26 ML {* |
28 if do_it then |
27 if do_it then |
29 generate_accessibility @{context} thy false "/tmp/mash_accessibility" |
28 generate_accessibility thy false "/tmp/mash_accessibility" |
30 else |
29 else |
31 () |
30 () |
32 *} |
31 *} |
33 |
32 |
34 ML {* |
33 ML {* |
38 () |
37 () |
39 *} |
38 *} |
40 |
39 |
41 ML {* |
40 ML {* |
42 if do_it then |
41 if do_it then |
43 generate_isa_dependencies @{context} thy false "/tmp/mash_isa_dependencies" |
42 generate_isa_dependencies thy false "/tmp/mash_isa_dependencies" |
44 else |
43 else |
45 () |
44 () |
46 *} |
45 *} |
47 |
46 |
48 ML {* |
47 ML {* |