remove unused lemma which was a direct consequence of tendsto_intros
add lemmas about nhds filter; tuned proof
add error messages for invalid inputs
merge
more complete set of lemmas wrt. image and composition
clarified print_local_facts;
clarified retrieve_generic: local error takes precedence, which is relevant for completion;
removed dead code;
more explicit treatment of verbose mode, which includes concealed entries;
clarified local facts;
tuned -- avoid vacuous reports;
tuned signature;
eliminated clones;
clarified completion ordering: prefer local names;
more markup;
minor tuning;
tuned markup;
normalising simp rules for compound operators
tuned proofs
more uniform alias vs. hide: proper check, allow to hide global names as well;
reject internal names, notably from Term.free_dummy_patterns;