tuning time slices in Sledgehammer (from Jasmin)

don't rerun tactic in minimizer -- this just redoes the same proof search again (from Jasmin)

rescale Sledgehammer slice factor (to allow smaller time slices for tactics like auto) (from Jasmin)

take chained facts into consideration in tactic hammer (from Jasmin)

initial work on Magnushammer-inspured tactic hammer (from Jasmin)

added lemmas monotone_on_sup_fun, monotone_on_inf_fun, antimonotone_on_sup_fun, antimonotone_on_inf_fun (thanks to Alexander Pach)

tuned options given to modern E Testing 500 goals of the HOL-Library session with a timeout of 30 s resulted in the following results. - No option: 9.4 % solved - Option "--auto": 45 % solved - Option "--auto-schedule": 46.8 % solved

weakened type class (thanks to Alexander Pach)

back to post-release mode -- after fork point;

added lemma

tuned

obsolete;

prefer inlined sfx.txt;

tuned signature: emphasize semantics;

proper File.standard_path for Windows: result of resources.source_file is platform_path (amending da1108a6d249);

added lemmas

merged

weakened type classes

merged

A few lemmas brought in from Polynomial_Interpolation

tuned;

more robust startup, notably on Ubuntu 24.04 with its strict policies on the "chrome-sandbox" executable;

more complete brackets, as in Isabelle/jEdit;

refrain from fancy GUI style (in contrast to 904b2144e9c5), which looks bad in Isabelle/VSCode;

move some settings to Isabelle repository (in contrast to fc363a3b690a), to facilitate changes without rebuilding the jedit component;

more robust jEdit Emacs Macros, based on patch #642 "bundled Emacs Macros are broken" (still open in jedit-5.7.0);

more accurate patch: change jEdit source directory and copy to installation directory;

tuned;

update find_facts_web component;

properly handle whitespace characters: must be escaped individually;

tuned UI;

tuned doc;