tuned output: formatting is pointless for proportional font;

clarified Tree_View.init_model: more uniform;

more robust update;

handle tree selection;

Output_Dockable: show search results as tree view;

clarified modules;

clarified signature;

clarified signature;

clarified signature and modules: without GUI change yet;

more operations, to support search within output panel;

tuned;

Introduced the function some_elem for grabbing an element from a non-empty set, and simplified the theorem the_elem_image_unique

Patch by Stepan Holub, plus tweaks

patch to vector_matrix_mult by Alexander Pach

try0: cleaned up output;

try0: insert extra facts into state instead of goal, since some methods (e.g. metis) won't work otherwise;

avoid informatik.tu-muenchen.de domain: soon to be discontinued;

renamed Discrete -> Discrete_Functions to avoid name clashes; new function names floor_log/sqrt to avoid long Discrete_Functions.log/sqrt

Use Var to maintain the difference between function and locale parameters

tuned

tuned proofs;

tuned proofs;

minor performance tuning: avoided repeated metric initialization;

tuned signature: more operations;

clarified signature;

more NEWS;

tuned proofs;

merged

enforce rebuild of Isabelle/ML and Isabelle/Scala;

update to jedit-20241115 (see also ecd62f7b3644 and d92d754b5dd9);