equal
deleted
inserted
replaced
6 |
6 |
7 theory MaSh_Import |
7 theory MaSh_Import |
8 imports MaSh_Export |
8 imports MaSh_Export |
9 uses "mash_import.ML" |
9 uses "mash_import.ML" |
10 begin |
10 begin |
|
11 |
|
12 sledgehammer_params |
|
13 [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, |
|
14 lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize] |
11 |
15 |
12 declare [[sledgehammer_instantiate_inducts]] |
16 declare [[sledgehammer_instantiate_inducts]] |
13 |
17 |
14 ML {* |
18 ML {* |
15 open MaSh_Import |
19 open MaSh_Import |