clarified modules;

tuned signature;

clarified modules: spell-checker in Pure;

added admin tool "isabelle build_vscode";

clarified options;

Tuned generation of elimination rules in function package

maintain decorations for document (model) and update it for each editor (view);

clarified messages (with improved scalability): legacy/error as diagnostics, writeln/information/warning/bad as tooltips (dynamic hover); discontinued obsolete "hover_message" decoration;

more robust;

tuned;

proper Text.Range.offside (NB: in Scala ~1 == -2);

tuned;

more general tooltips, with uniform info range handling;

tuned;

more generic colors;

tuned whitespace;

proper color;

more generic colors;

more ambitious timing, to compensate general protocol delays;

decorations for dotted underline: less intrusive; tuned;

more generic rendering;

proper reset of published decorations: initial value is Nil, afterwards it is a list of canonical length and order;

always invoke output: pending_output may be present due to other reasons;

tuned signature;

tuned;

simplified;

publish output more thoroughly;

potentially redundant pending_output, for the sake of uniformity and reactivity;

tuned;

tuned;

more robust treatment of pending input/output: these are often correlated; no decorations for invisible node;

merged

added numeral_powr_numeral

merged

clarified pretty margin;

more general hover_message (see also JEdit_Rendering.tooltip_message);

clarified signature;

decorations for background and foreground colors;

tight protocol messages;

tuned signature;

symbolic Rendering.Color; clarified modules;

tuned;

Knaster-Tarski fixed point theorem and Galois Connections.

evade odd version conflicts for batch build (e.g. "vsce package");

more robust Uri comparison, notably on Windows;

tuned;

publish decorations like diagnostics; Markup.BAD is decoration, not error message;

support for decorations;

clarified signature;

clarified versions;

clarified LICENSE;

more robust: tmp files might get deleted concurrently in ML vs. Scala process;

clarified fonts;

tuned;

clarified errors;

tuned;

clarified;

tuned message;

tuned;

tuned;

handler for Isabelle version;

tuned;

handler for Isabelle fonts;

more operations;

clarified modules;

clarified signature;

misc tuning and modernization;

improved performance of remove, e.g. relevant for Theories_Dockable.purge;

more uniform platform settings;

more detailed platform information;

proper Isabelle/Scala tool;

more operations;

tuned;

merged;

tuned message;

tidied some messy proofs

Merge

Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands

more tests;

stripped unused / obsolete material

merged

more links;

clarified priority: zero can mean unknown/long or irrelevant/short time;

absent timing information means zero, according to 0070053570c4, f235646b1b73;

Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.

clarified defaults;

tuned whitespace;

tuned;

clarified defaults;

more operations;

tuned signature;

re-established AFP entry for FinFuns as library

clarified comment

added multiset lemma

added multiset lemma

back to Poly/ML 5.6 until odd memory management problems are sorted out;

avoid Unicode that conflicts with Isabelle symbol rendering;

more correct wording

explicit dynamic context for gap-bridging function

more precise NEWS and CONTRIBUTORS

basic documentation for computations

The Great Picard Theorem

New theory about Winding Numbers

new lemmas about segments, etc. Also recast some theorems to use Union rather than general set comprehensions

some new material, also recasting some theorems using “obtains”

Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion

backed out unintended effects of 8355a6e2df79 in src/HOL/Algebra

more complete program generation in presence of dictionaries

removed obsolete test -- coincides with mainline version;

updated to polyml-5.7 pre-release from repository;

use the cancellation simprocs directly

don't activate simproc on cancel_comm_monoid_add

cancellation simprocs generalising the multiset simprocs

adding simplification patterns to multiset simprocs

renaming multiset simprocs

implicit eta contraction for preprocessed terms avoids unintended implicit eta expansion

explicit operations for executable primality checks

more fun without recdef

merged

proper transaction for PostgreSQL;