clarified signature;

clarified signature: name according to db model without Sessions.Structure/Deps;

added lemmas

tuned

spelling;

tuned;

read theory with PIDE markup from session database;

clarified signature: provide XZ.Cache where Export.Entry is created;

tuned signature;

tuned signature;

clarified exports;

clarified markup (refining 1c59b555ac4a);

clarified markup: support more completion, e.g. within ROOTS;

more accurate markup (refining 1c59b555ac4a);

tuned signature --- more operations;

clarified File_Format.detect: needs to operate on full node name;

more accurate syntax, following Sessions.parse_roots in Scala;

PIDE support for session ROOTS;

more robust;

more Unicode;

eliminated odd "Read_me";

eliminated odd "Read_me";

tuned signature;

silently ignore markup that starts out as singularity, e.g. <language/> from empty ML file;

moved some lemmas from AFP to distribution

avoid duplicate entries: snippet_command is defined within node;

merged

proper span position for blobs in batch-build (but: practically irrelevant);

proper treatment of singleton Position.Offset within blob (amending cb9d5af781b4);

more robust batch-build;

tuned;

tuned signature;

clarified signature;

tuned signature;

clarified signature;

tuned;

clarified signature;

clarified signature, notably access to blob files;

support for PIDE markup for auxiliary files ("blobs"); clarified files of theory Pure;

tuned;

clarified signature --- more explicit types;

merged

removed session name

merged

NEWS

merged

summarized structural and ordering invariant for trees

Total correctness examples by Walter Guttmann

Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann

tuned

Highlight that 'intro_locales' and 'trace_locales' are useful debug features, plus minor clarifications.

merged

added abbrev

merged

clarified signature --- more positions;

clarified signature;

tuned proof preplay to explicitly refer to Z3 backend

A bunch of suggestions from Pedro Sánchez Terraf

merged

merged

tweaked

obsolete -- done by Isabelle/PIDE/ML;

tuned whitespace --- avoid TABs;

updated to Haskell stack-2.5.1, stackage lts-16.12, ghc-8.8.4;

updated to postgresql-42.2.18;

updated to jfreechart-1.5.1;

updated to current cygwin-20201130, after 3.1.7-1 from 24-Aug-2020;

Added tag Isabelle2021-RC0 for changeset 21ff9c1a4644

more Isabelle fonts, notably for PanelWindowContainer buttons with Windows L&F;

merged

Path.implode_symbolic as in ML;

proper source symbols in persistent data;

more completion;

tuned signature;

restrict report redirection to current node;

clarified parser;

tuned signature;

proper positions for inlined command messages, e.g. for completion within theory header;

tuned signature;

clarified modules;

tuned signature;

clarified checks (see f34f5c057c9e);

clarified signature;

tuned comments;

tuned;

typo

more on signed division

clarified files;

tuned whitespace;

clarified parsing vs. semantic errors;

clarified signature;

added document antiquotation @{tool}; formal check of isabelle tools via Isabelle/Scala;

more robust isabelle_scala_files; clarified evaluation;

avoid conflicting base names;

clarified protocol: Doc.check at run-time via Scala function;

more antiquotations (reverting 4df341249348);

tuned;

tuned signature --- more explicit types;

more positions;

support for Scala compile-time positions;

clarified modules;

more robust (amending a4d7da18ac5c);

merged

merged

More removal of apply

merged

more flexible syntax for theory load commands via Isabelle/Scala;

clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically; propagate blob src_path from Scala to ML; clarified signature;

proper structural equality;

more explicit types;

unused (see 7634d33c1a79);

clarified signature;

clarified modules;

clarified file names;

tuned signature;

refined syntax for bundle mixins for locale and class specifications

store timings for used_theories in canonical order, with reconstructed store.read_theories;

merged

merged

Stepan Holub's stronger version of comm_append_are_replicate, and a de-applied Word.thy