Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.

subdegree/shift/cutoff and Euclidean ring instance for formal power series

prefer static Font -- evade spontaneous change of TextField.font seen with Metal L&F in Plugin Options / Isabelle / General / Apply;

uniform mandatory qualifier for all locale expressions, including 'statespace' parent; removed obsolete '!' syntax;

qualifier is mandatory by default;

prefer explicit State panel;

suppress already persistent state output as well;

added option timeout_scale;

syntactic completion may supersede semantic completion, e.g. relevant for "\undefined" vs. "undefined" in ML;

clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);

tuned;

less confusing markup;

added @{undefined} with somewhat undefined symbol;

ML cartouches via control antiquotation;

more formal treatment of control symbols;

more antiquotations;

more antiquotations;

retain traditional rendering of \<paragraph>;

added glyphs 0x204b, 0x2b1a from DejaVuSansMono;

tuned;

tuned

tuned

updating options to verit

isabelle update_cartouches -c -t;