more NEWS;

clarified component name and content for FIND_FACTS_INDEXES: prefer db with compression;

more robust shasum: proper relative file names; rebuild find_facts_web-20250223;

tuned output;

tuned NEWS;

more NEWS;

Added tag Isabelle2025-RC3 for changeset 52290d6ab92d

merged

Some new lemmas and some tidying

tuned code and signature of try0

tuned: restricted visibility of definitions

tuned signature

added type names and type annotations

tuned to use stronger type Time.time

compute right timeout (from Jasmin)

clarify inteaction of tactic hammer and suggest_of=smart (from Jasmin)

tentatively catch Interrupt_Breakdown in Sledgehammer (from Jasmin)

more tactics in tactic hammer (from Jasmin)

tactic hammer documentation (from Jasmin)

tuned time slicing (from Jasmin)

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;

clarified;

limit size of overly large blocks;

proper synonyms: special characters need to be escaped;

tuned;

merged

serve Browser_Info in Find_Facts, addressable by relative paths (instead of absolute URLs that may have inconsistent data);

use bundled browser_info.db for Find_Facts in release;

clarified cli; always clean old index;