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;