tuned;

tuned signature;

tuned signature;

clarified key event propagation, in accordance to outer_key_listener;

allow implicit semantic completion, notably after delay that exceeds usual round-trip time; clarified isabelle.completion action: already open popup is re-opened and thus updated;

reject internal names, notably from Term.free_dummy_patterns;

more uniform alias vs. hide: proper check, allow to hide global names as well;

tuned proofs

normalising simp rules for compound operators

tuned markup;

minor tuning;

more markup;

clarified completion ordering: prefer local names;

tuned signature; eliminated clones;

tuned -- avoid vacuous reports;

clarified local facts;

more explicit treatment of verbose mode, which includes concealed entries;

removed dead code;

clarified retrieve_generic: local error takes precedence, which is relevant for completion;

clarified print_local_facts;

more complete set of lemmas wrt. image and composition

merge

add error messages for invalid inputs

add lemmas about nhds filter; tuned proof

remove unused lemma which was a direct consequence of tendsto_intros

merged

merged

prefer more robust Synchronized.var;

discontinued somewhat pointless "thy_script" keyword kind;

conceal improper cases, e.g. relevant for completion (and potentially for markup);

conceal somewhat obscure internal facts, e.g. relevant for 'print_theorems', 'find_theorems';

more accurate resolution of hybrid facts, which actually changes the sort order of results;