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;

generate browser_info.db in Find_Facts;

clarified: more operations;

use core.properties for Solr index meta info;

tuned;

clarified persistent data: digest may help to synchronize files, without requiring read / uncompress;

proper treatment of empty content, which is never compressed;

proper $ISABELLE_BROWSER_INFO_SYSTEM for "isabelle build -o system_heaps";

merged

clarified signature: more explicit operations;

tuned;

tuned signature: more operations;

expose bundle $ISABELLE_BROWSER_INFO_LIBRARY via HTTP;

more operations;

tuned signature: more explicit operations;

support for browser_info.db --- requires approx. 10s to compress 1.2GB to 152MB;

more operations;

tuned signature;