equal
deleted
inserted
replaced
9 begin |
9 begin |
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_relevant = 40, strict, dont_slice, type_enc = mono_native, |
14 [provers = spass, max_relevant = 32, strict, dont_slice, type_enc = mono_native, |
15 lam_trans = combs_and_lifting, timeout = 1, dont_preplay, minimize] |
15 lam_trans = combs_and_lifting, timeout = 2, dont_preplay, minimize] |
16 |
16 |
17 ML {* |
17 ML {* |
18 open MaSh_Export |
18 open MaSh_Export |
19 *} |
19 *} |
20 |
20 |
55 () |
55 () |
56 *} |
56 *} |
57 |
57 |
58 ML {* |
58 ML {* |
59 if do_it then |
59 if do_it then |
60 generate_commands @{context} params thys (prefix ^ "mash_commands") |
60 generate_isar_commands @{context} prover thys (prefix ^ "mash_commands") |
61 else |
61 else |
62 () |
62 () |
63 *} |
63 *} |
64 |
64 |
65 ML {* |
65 ML {* |
74 generate_atp_dependencies @{context} params thys false (prefix ^ "mash_atp_dependencies") |
74 generate_atp_dependencies @{context} params thys false (prefix ^ "mash_atp_dependencies") |
75 else |
75 else |
76 () |
76 () |
77 *} |
77 *} |
78 |
78 |
|
79 ML {* |
|
80 if do_it then |
|
81 generate_atp_commands @{context} params thys (prefix ^ "mash_atp_commands") |
|
82 else |
|
83 () |
|
84 *} |
|
85 |
79 end |
86 end |