merged

try proof method "order" in Sledgehammer's proof reconstruction

added Mirabelle action "order"

renamed lemma antisymp_on_reflcp to antisymp_on_reflclp

tuned proof

added lemma order_reflclp_if_transp_and_asymp

added lemmas antisym_on_reflcl_if_asym_on and antisymp_on_reflclp_if_asymp_on

HOL-Library: added modulo/congruence for real numbers

only print schedule if relevant;

remove laziness: no need, and errors during initialization loop with close();

more general definition of meromorphicity; Weierstraß factorisation theorem

always provide build_database_server option in benchmark command;

always check if node is defined, e.g. for exists_next operation wit empty schedule;

fixed typo

disable taskset for now: performance impact is negative;

allow specifying initial schedule;

clarify use of num_threads vs. max_cpus;

clarified host: pre-load max threads;

clarified: more operations;

added alias wfp for wfP

merged

added lemmas wf_on_antimono, wf_on_antimono_strong, wfp_on_antimono, wfp_on_antimono_strong, wf_on_subset, and wfp_on_subset

start scheduled jobs earlier, if possible;

tuned proofs

added lemmas wfP_iff_ex_minimal, wf_iff_ex_minimal, wf_onE_pf, wf_onI_pf, wf_on_iff_ex_minimal, and wfp_on_iff_ex_minimal

merged

added definitions wf_on and wfp_on as restricted versions of wf and wfP respectively

read/write proper schedule date (amending 9da3019e1ee5);

allow read/write of schedule in build (read via option, write from tool);

file representation for schedule (e.g., for generating from external tool);