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

simplify proof of Bseq_mono_convergent

merged

replace lemma expi_imaginary with reoriented lemma cis_conv_exp

remove redundant lemmas expi_add and expi_zero

remove redundant lemmas about LIMSEQ

introduce abbreviation 'int' earlier in Int.thy

remove unused assumptions from natceiling lemmas

move lemmas nat_le_iff and nat_mono into Int.thy

eliminated markup for plain identifiers (frequent but insignificant); reduced "black" markup (outer string etc. takes care of it already);