contributor

added simproc for cont

clarify Sledgehammer instantiations without preplay (dont_preplay option and tactic provers)

more robust (amending 4ca84abb16ef): Main_Plugin.start() could happen on other thread, e.g. when $JEDIT_SETTINGS/recent.xml refers to "isabelle-export:" URL;

added lemma

merged

clarified settings: these are setup defaults, not necessarily the installed version;

provide "isabelle caddy_setup" and "isabelle caddy"; proper go-1.24.1 as required by xcaddy-0.4.4;

update to current go-1.24.3;

tuned;

clarified signature and modules;

tuned comments;

clarified signature;

prefer official precise attribute

Kleene's fixpoint thm

merged

Kleene for lfp

A new lemma

merged

A few more useful lemmas (about topology)

more theorems

merged

two more lemmas from the AFP

new lemma

consolidate input syntax

More type class things

executable sorted_list_of_multiset

Tweaking the ordered semiring type classes

merged

New type classes unboundedx_dense_order, ordered_semiring_1, ordered_semiring_strict and related material from Complex_Bounded_Operators

merged

more robust output: no markup as last resort;

clarified signature: more scalable output --- avoid adhoc string concatenations after Pretty.string_of;

clarified signature: more scalable output;

tuned;

more scalable: discontinue odd shortcuts from 6b3739fee456, which produce bulky strings internally;

tuned

preserved facts order in Sledgehammer's linear minimizer

merged

more scalable;

more scalable;

more scalable output;

tuned document text;

more navigator positions, after BufferUpdate.LOADED and Buffer.CARET_POSITIONED (see also e48b3ddc4810);

pass "using" facts as parameters to metis in try0

clarified signature

proper command message for Sledgehammer's proof methods

merged

tuned metis_instantiate (import types, support unfixed variables)

merged

merged

update NEWS;

proper painting of menu accelerator in dark mode;

clarified patches;

more uniform init_lafs();

tuned signature, following 1033ed5d3972;

update jedit component;

tuned signature -- requires to update jedit component;

tuned GUI -- requires to update jedit component;

more accurate GUI painting;

clarified GUI calculations for icons;

tuned;

more FlatLaf operations (following 35d176c50867) -- requires to update jedit component;

more accurate GUI property (amending 49ca1a40c04a) -- requires to update jedit component;

more accurate macOS L&F (see also efc58b56a6c7);

provide FlatMac themes (see also FlatLaf 3.0);

tuned imports;

more FlatLaf operations;

clarified signature;

updated to jedit-20250417; removed obsolete idea-icons-20250415: already bundled in jedit component; clarified JEdit_Lib.load_icon, following afa1c2d485ae and 6d5a169c3a22;

tuned icons -- requires to update jedit component;

tuned icons, notably for menus -- requires to update jedit component;

bundle idea-icons-20250415 with jedit -- requires to update jedit component;

bundle SVG tango icons with jedit -- requires to update jedit component; revise jedit_gui.props: prefer SVG in most situations; replace hardwired icon names by props;

support scaled svg icons directly in GUIUtilities.loadIcon -- requires to update jedit component;

update idea-icons: prefer scalable SVG;

support for SVG icons via com.formdev.flatlaf.extras.FlatSVGIcon from flatlaf-extras (which is based on JSVG);

misc tuning and clarification;

update to flatlaf-3.6, with native library support on all platforms;

injectivity results about sin, cos, cis

a few small lemmas for HOL and HOL-Analysis

some material on power series and infinite products

merged

merged

More tidying and some variable renaming

dropped problematic code equation for multisets for RBT code testing

removed possible problematic dependency in HOL-Library.Multiset

HOL-Library: multisets of a given size

some facts about derivatives of products

more about formal convergence of power series

removed name clash in some lemmas

added orphaned theory to HOL-Analysis

some facts about power series

moved some lemmas to where they fit better

more efficient conversions for symbolic representations

notes on bit shift rewrites

explicit case rule

more lemmas

more lemmas

explicit check for computations on word type

more tidying

merged

tidied more proofs

removed duplicate lemmas

lots of lemmas for HOL, HOL-{Complex_}Analysis, HOL-Number_Theory

new lemmas for HOL-Complex_Analysis; overhaul of isolated_zeros

official theory for using bit shift operations for ordinary arithmetic if feasible

corrected operation

tuned whitespace

Simplified old proofs

merged

update to recent MSYS2 / MinGW, which also works via Cygwin;

tuned

tuned

tuned

tuned

revamped generation of functions

NEWS

typo

tuned

merged

Tidied some proofs

merged

clarified signature: more uniform;

tuned;

more accurate MinGW path conversion: support locations outside of mingw.root; uniform treatment of GMP, including Windows;

tuned messages;

tuned;

more uniform directory structure: Windows DLLs are treated like binaries;

tuned messages;

more uniform make_polyml_gmp vs. make_polyml;

clarified options: explicit use of existing GMP library;

clarified default options: prefer GMP from source;

Tidied more messy old proofs

more tidying and simplifying

merged

tidying some old proofs

Generalised a lemma and added another

merged

more robust;

more robust;

clarified GMP build options, notably for Windows;

more robust access to GMP library that is provided here;

clarified command-line;

tuned;

tuned;

more uniform verbose mode;

more explicit build stages;

tuned;

more uniform platform_context.execute;

more robust shell script;

tuned comments;

A couple of new lemmas

merged

clarified Windows: always use MinGW version (it is unclear how to build libgmp-10.dll);

clarified signature: fewer warnings in IntelliJ IDEA;

tuned: prefer explicit Bash.exports;

tuned signature;

clarified signature: more explicit type Platform_Context;

added option -G to build GMP library from sources;

Another Eberl lemma plus tidying

Another of Manuel's theorems

merged

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;

tuned: fewer warnings in IntelliJ IDEA;

tuned GUI: follow org.gjt.sp.jedit.search.SearchBar;

merged

Inserted more of Manuel Eberl's material

merged

tuned NEWS

added proof method "iprover" to try0

added a user-configurable schedule to try0

Lemmas from Manuel Eberl's Q_Analogues

Added lemma

more on sorting

tuned whitespaces

merged

Some generalisations (mostly at the level of type classes) by Alexander Pach

tuned

tuned

tuned

tuned

tuned signature

garbage collection

removed old Vampire configuration from Sledgehammer

removed old E configuration from Sledgehammer

removed unused function

tuned namespace organisation

optional external files as code modules

proper markup for target language code

tuned

tuned

tuned

tuned

spelling

tuned

removed debug commands

merged

refactored tactic-based provers in sledgehammer to use Try0 module

tuned stringification of proof method in try0

simplified implementation of the_signed_int