tuned;

try0: pass tagged thms for better control;

clarified: proper return type;

improve try0: solve multiple subgoals at once, if possible;

tuned: unused parameter;

tuned

better termination behaviour

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;

tuned names;

more robust;

clarified signature;

unused;

clarified signature: more explicit types;

tuned GUI;

tuned;

clarified signature;

clarified signature;

tuned imports;

tuned: remove redundant checks;

tuned;

clarified modules;

clarified signature;

clarified signature;

clarified signature;

tuned: fewer warnings in IntelliJ IDEA;

clarified signature;

clarified modules: more re-usable;

proper protocol messages (amending 7a1f9e571046);

clarified treatment of caret_range: better support for multiple (unrelated) selections;

tuned whitespace;

support incremental isabelle.select-structure --- like select-block, but based on selection instead of caret;

clarified rendering: entity acts as atomic notation / expression;

more rendering for Markup.COMMAND_SPAN, following Rendering.structure_elements;

more NEWS;

merged

support Isabelle/jEdit action isabelle.select_structure; update component jedit-20241101;

more operations;

clarified text;

update to jedit5.7.0;

GUI option "editor_auto_hovering" for Output panel;

update to scala-3.3.4 LTS;

removed obsolete markup for "open_block" (see also d5ad89fda714): Isabelle/Scala directly supports XML.Elem pretty-printing;

Library material from Eberl's Parallel_Shear_Sort

Trying to clean up these horribly ugly old proofs, but the requirement of constructivity makes it very difficult

use automatically generated time function in HOL-Data_Structures.Selection

merged

better time_functions (let)

less hidden configuration;

proper passwordless smtp check: must be null;

adjusted documentation

more attribute tuning

tuned attributes

merged

added lemmas

tuned proofs;

tuned NEWS;

markup for "..." notation; clarified signature;

more robust: avoid non-authentic translations;

tuned whitespace of sources;

update documentation; tuned typesetting;

tuned;

update documentation: print mode "latex" only affects syntax tables, but output of symbols;

misc tuning and clarification;

clarified section structure;

tuned;

tuned;

tuned;