equal
deleted
inserted
replaced
9 uses "mash_export.ML" |
9 uses "mash_export.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??, |
14 lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize] |
14 lam_trans = combs_and_lifting, timeout = 1, dont_preplay, minimize] |
15 |
15 |
16 ML {* |
16 ML {* |
17 open MaSh_Export |
17 open MaSh_Export |
18 *} |
18 *} |
19 |
19 |
64 generate_atp_dependencies @{context} params thy false "/tmp/mash_atp_dependencies" |
64 generate_atp_dependencies @{context} params thy false "/tmp/mash_atp_dependencies" |
65 else |
65 else |
66 () |
66 () |
67 *} |
67 *} |
68 |
68 |
69 |
|
70 end |
69 end |