optimize special case according to Library.merge (see also 8fbc355100f2, 520872460b7b);

tuned colors;

prefer standard Proof_Context.transfer, with theory stamp transfer (should now work thanks to purely functional theory, without Theory.copy etc.);

more robust registration of code equations

be consistent and produce always rep_eq with =

publish a useful function

don't be so aggresive for a public test function and raise only BAD_THM instead of ERROR

add missing attributes

Lemmas about Reals, norm, etc., and cleaner variants of existing ones

A few lemmas about summations, etc.

merged

tuned;

tuned messages -- prefer quote before Position.here, which might be just \<here>;

clarified ML language flags;

clarified painting of invisible caret, e.g. focus change due to popup;

tuned signature -- weaker type requirement;

paint completion range of active popup;

tuned messages;

clarified Token.range_of in accordance to Symbol_Pos.range; eliminated redundant Position.set_range, which is already included in Position.range;

tuned signature;

clarified interaction with dead variables in the composition of BNFs

added BNF cache (within one definition)

updated docs

optimized 'bnf_of_typ' further w.r.t. dead variables

optimization of 'bnf_of_typ' if all variables are dead

improved accounting for dead variables when naming set functions (refines d71c2737ee21)

added explicit killing

more precise error message

reuse same parser for '(co)datatype(_new)' as for 'bnf_decl'

tuned message;