equal
deleted
inserted
replaced
4 |
4 |
5 header {* MaSh Evaluation Driver *} |
5 header {* MaSh Evaluation Driver *} |
6 |
6 |
7 theory MaSh_Eval |
7 theory MaSh_Eval |
8 imports Complex_Main |
8 imports Complex_Main |
9 uses "mash_eval.ML" |
|
10 begin |
9 begin |
|
10 |
|
11 ML_file "mash_eval.ML" |
11 |
12 |
12 sledgehammer_params |
13 sledgehammer_params |
13 [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, |
14 [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, |
14 lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize] |
15 lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize] |
15 |
16 |