Re: [isabelle] sledgehammer in RC4



Hi Jasmine,

I'm running in a VBox virtual machine on a MacPro that has 2 cores

> 1. How many cores does your machine have?
The VM is set with 2 CPUs

> 2. What is the value reported by ML {* Multithreading.max_threads_value () *} ?
2

> 3. Do you use Proof General or jEdit/PIDE?
Proof General

> 4. How do you invoke Sledgehammer? Do you type "sledgehammer" in the editor window or use the new jEdit Sledgehammer panel?
I type "sledgehammer"

> 5. What is the output of the "sledgehammer_params" command?
Default parameters for Sledgehammer:
blocking = false
debug = false
fact_filter = smart
fact_thresholds = 0.45 0.85
isar_compress = 10
isar_proofs = smart
isar_try0 = true
lam_trans = smart
learn = true
max_facts = smart
max_mono_iters = smart
max_new_mono_instances = smart
minimize = smart
overlord = false
preplay_timeout = 3
provers = e spass
slice = true
spy = false
strict = false
timeout = 30
type_enc = smart
uncurried_aliases = smart
verbose = false

Thanks,
Randy




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.