More of Manuel's material

removed iprover from try0 because its name is clashing with iProver in Sledgehammer

expanded Sledgehammer's schedule (loosely inspired by "Hammering without ATPs" evaluation)

added try0's schedule to sledgehammer's schedule

clarified signature

clarified variable names

tuned

use existing implementations of bit operations if nat is implemented by target-language integer

merged

more comments;

mandatory option --enable-ho (see also fc5f10691147);

update to e-3.2, which is actually 3.2.5; enforce rebuild of Isabelle/ML;

reflect nested lists in variables names

Simplified lemma (as suggetsed by Stepan Holub)

incorporate target-language integer implementation of bit shifts into Main

represent constants with explicit typargs to avoid false positives for equality approximations like ‹card UNIV === card UNIV›

restored type reconstruction for nbe: remaining type variables must remain schematic for checking

tuned

merged

NEWS;

more documentation;

update jedit component;

more navigator positions;

clarified navigator events: avoid excessive 0 positions;

more robust: make double-sure that get_text does not crash (see on non-existent file);

more uniform treatment of open buffer vs. loaded file (NB: setCaretPosition includes selectionNone);

proper hyperlink column (amending 6898054035d6);

tuned: setCaretPosition already includes selectNone;

tuned signature;

clarified history: eliminate pointless var _current;

clarified target position: line start + offset (or column); more uniform treatment of open buffer vs. loaded file;

tuned source structure;

eliminated patch: imitate jEdit.gotoMarker more directly;

tuned;

tuned signature: proper private vars;

tuned signature;

unused;

suppress NavigatorPlugin and its dependencies -- requires to update jedit component;

prefer search bar (with navigation buttons) over old-fashioned tool bar -- requires to update jedit component;

add navigation buttons to search bar, depending on property "navigate-toolbar" -- requires to update jedit component;

remove goto_buffer in favour of uniform goto_file;

support goto_file / hyperlink_file with offset; clarified signature;

update jedit component;

unused (see also 1046a69fabaa);

prefer generic action names, to be injected into jEdit codebase eventually;

support for jEdit.openFiles with "+offset:" specification --- requires to update jedit component;

more accurate navigator position;

clarified actions and keyboard shortcuts --- requires to update jedit component;

tuned GUI (see also a01c1f874362) --- requires to update jedit component;

support for navigation, independently of Navigator plugin;

misc tuning: more modular message dispatch;

provide component for https://files.sketis.net/Isabelle_Naproche-20250328

tuned signature;

clarified signature;

tuned (see also 20b261654e33);

more robust;