equal
deleted
inserted
replaced
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 = lifting, timeout = 2, dont_preplay, minimize] |
15 lam_trans = lifting, timeout = 2, dont_preplay, minimize] |
16 |
16 |
17 declare [[sledgehammer_fact_duplicates = true]] |
17 declare [[sledgehammer_fact_duplicates = true]] |
18 declare [[sledgehammer_instantiate_inducts = false]] |
|
19 |
18 |
20 hide_fact (open) HOL.ext |
19 hide_fact (open) HOL.ext |
21 |
20 |
22 ML \<open> |
21 ML \<open> |
23 Multithreading.max_threads () |
22 Multithreading.max_threads () |