uniform name T_f for closed-form lemmas for function T_f

More time for primitive functions

merged Reverse into Time_Funs

tuned proofs;

tuned description: plain text documentation is also supported;

merged

update to jdk-21.0.5; enforce rebuild of Isabelle/ML and Isabelle/Scala;

misc tuning and clarification: Doc.Entry supports both plain files and pdf documents; recover plain file support from 488c7e8923b2;

tuned proofs

added missing definitions

tuned proofs; more Isabelle symbols;

clarified modules;

support value-oriented Font_Metric, e.g. for caching Pretty output;

tuned;

unused;

tuned;

tuned;

clarified signature; clarified modules;

more accurate Symbol.Metric, following 6eccae338770;

tuned rendering, notably for HiDPI on Linux (see also ca7e2c21b104);

proper parentheses, for the sake of IntelliJ IDEA;

clarified modules;

clarified signature;

tuned proofs;

tuned GUI (again, see 0521e65af41e);

tuned proofs;

tuned;

tuned comments;

clarified signature;

tuned;