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;

tuned -- command 'text' was localized some years ago;

back to a form of hybrid facts, to reduce performance impact of ed92ce2ac88e;

just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.); more thorough background_notes: distribute global notes to all contexts;

more frugal recording of changes: join merely requires information from one side; tuned;

do not test details of error messages;

minor tuning -- NB: props are usually empty for global facts;

even smarter Path.smart_implode;

added ML antiquotation @{path};

clarified Path.smart_implode; more informative report and rendering;

generalization of differential_zero_maxmin to class real_normed_vector

delayed construction of command (and of noncommercial check) + tuning

tuning

consolidate consecutive steps that prove the same formula

remove '__' skolem suffixes before showing terms to users

undo rewrite rules (e.g. for 'fun_app') in Isar

debugging stuff

more simplification of trivial steps

tuning