cleanup "simple" type encodings

merge

HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem.

tuning

drop more type arguments soundly, when they can be deduced from the arg types

bulk reports for improved message throughput;

bulk reports for improved message throughput;

tuned signature;

more specific message channels to avoid potential bottle-neck of raw_messages;

buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;

more abstract receiver interface;

flush after Output.raw_message (and init message) for reduced latency of important protocol events;

convert lemma cos_is_zero to Isar-style

merged

convert lemma sin_gt_zero to Isar style; remove duplicate lemma sin_gt_zero1;

modify lemma sums_group, and shorten proofs that use it

generalize some lemmas

add lemmas cos_arctan and sin_arctan

tuned indentation

more visible outdated_color;

commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;

tuned imports;

fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"

tuned

tuned

filter out all schematic theorems if the problem contains no ground constants

merged

tuned comments