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

merged

tuned

removed assumptions in lemma (Stepan Holub)

merged

more exports from rendering; suppress empty exports;

clarified signature;

clarified options: batch-build has pide_reports disabled by default (requires significant resources);

tuned;

proper return code for more errors (amending d892f6d66402);

more exports, as in "isabelle dump";

tuned;

clarified signature;

clarified signature: initial markup is_empty, not init_markup;

clarified signature: prefer high-level Snapshot over low-level Command.State;

tuned;

more strict;

clarified signature;

tuned;

clarified signature;

clarified signature --- avoid repeated open_database on server;

renaming

merged

recovered document output from 6bc199a70bf9;

clarified command_timings protocol;

more robust: include reports from Thy_Output.present_thy/output_document;

more complete report positions, notably for command 'back' (amending eca176f773e0);

tuned signature;

clarified signature;

unused;

unused;

tuned;

removed pointless case: messages should always carry proper position;

clarified names;

eliminated pointless transaction;

tuned signature;

clarified document_output vs. progress;

clarified: more uniform;

more robust;

clarified signature and database layout;

clarified messages;

unused (see ac7ae5067783, 1c451e5c145f);

unused;

support for PIDE markup in batch build (inactive due to pide_reports=false);