equal
deleted
inserted
replaced
10 |
10 |
11 ML_file "mash_export.ML" |
11 ML_file "mash_export.ML" |
12 |
12 |
13 sledgehammer_params |
13 sledgehammer_params |
14 [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native, |
14 [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native, |
15 lam_trans = combs_and_lifting, timeout = 2, dont_preplay, minimize] |
15 lam_trans = lifting, timeout = 2, dont_preplay, minimize] |
16 |
16 |
17 declare [[sledgehammer_instantiate_inducts]] |
17 declare [[sledgehammer_instantiate_inducts = false]] |
18 |
18 |
19 ML {* |
19 ML {* |
20 !Multithreading.max_threads |
20 !Multithreading.max_threads |
21 *} |
21 *} |
22 |
22 |
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 thys = [@{theory List}] |
29 val thys = [@{theory List}] |
30 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} [] |
30 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} [] |
31 val prover = hd provers |
31 val prover = hd provers |
32 val max_suggestions = 1024 |
32 val max_suggestions = 1536 |
33 val dir = "List" |
33 val dir = "List" |
34 val prefix = "/tmp/" ^ dir ^ "/" |
34 val prefix = "/tmp/" ^ dir ^ "/" |
35 *} |
35 *} |
36 |
36 |
37 ML {* |
37 ML {* |