avoid "Code" as structure name (cf. 3bc39cfe27fe)

remove duplicate copy of lemma sqrt_add_le_add_sqrt

remove redundant lemma real_sum_squared_expand in favor of power2_sum

remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex

merged

add lemmas about arctan; simplify some proofs about arctan;

convert lemma cos_total to Isar-style proof

added new lemmas

updated Sledgehammer's docs

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;