added lemmas

merged

updated for release;

Added tag Isabelle2021-RC4 for changeset 2ab14dbc6feb

provide naproche-20210201;

clarified messages;

more parallel;

more parallel;

contributors

hide the internal abbreviations MR and MB

optimize RBT_Impl

merged

more robust HTML output: non-balanced bsub/esub are shown verbatim, e.g. within mixfix declarations (due to extra markup);

tuned signature: more types;

clarified signature: proper order;

clarified signature: more explicit types;

tuned;

clarified signature: no symbol markup within XML attributes;

clarified signature;

tuned signature;

bundle more libraries from scala-2.12.x, notably for Isabelle/MMT;

provide naproche-20210129;

more robust type signatures, notably for the sake of haskell-stack-trace-plugin-0.1.1.1;

tuned signature (e.g. see HTML.control_block in Isabelle/Scala);

proper Isabelle environment (amending 31fbde3baa97);

updated to jdk-15.0.2+7;

follow Phabricator update 2021 Week 4;

more NEWS;

more uniform directory layout for macOS; uniform Isabelle_app executable + lib/scripts/Isabelle_app for Linux and macOS; proper support for Apple "Files and Folders" security via x86_64-darwin executable (which is still able to launch arm64-darwin Java);

more generic Isabelle_app;

prefer dynamic linking: platform is always x86_64 (see 373dcdd363dc);

more robust;

tuned;

tuned;

provide jdk-11.0.10+9.tar.gz LTS for testing (inactive);

Simpler proof

more robust: support other_isabelle.init_settings for build_history before b93404a4c3dd;

more robust: defer error in sessions structure to build process;

merged, with minor edits: Admin/PLATFORMS, CONTRIBUTORS;

Added tag Isabelle2021-RC3 for changeset 02422c9add5e

provide naproche-20210124 (inactive);

follow stackage update;

tuned name, e.g. relevant for Naproche-SAD debugging in Isabelle/jEdit;

more operations for client connection;

fewer warnings, notably in Naproche-SAD;

suppress bundled Naproche-SAD component: it is in conflict with building the same from sources;

more robust etc/settings;

IDE support for Naproche-SAD;

proper path;

support isabelle components -u and -x;

proper typescript version, required for "vsce package";

auto-update;

auto-update;

proper type constraint;

VSCode extension for official Isabelle release;

proper message;

unused;

proper heap_free;

suppress markup for literal tokens with block control symbols, for better PIDE/HTML output (see also d15fe10593ff);

clarified documentation concerning macOS Big Sur;

more systematic java-gui-setup, also for "isabelle jedit" command-line tool;

updated to flatlaf-1.0-rc1;

tuned;

tuned proofs;

tuned;

obsolete;

clarified platforms;

more NEWS;

workaround for Big Sur fullscreen mode: better support for JDialog windows (e.g. Find on top of main View);

clarified app identification, potentially relevant for macOS "defaults";

updated documentation: HIDPI works smoothly thanks to FlatLaf;

updated for release;

updated screenshot;

clarified reports before errors: support completion of bibtex entries in Isabelle/Scala (amending d01ea9e3bd2d);

tuned;

proper theory_long_name;

updated screenshots;

more robust GUI, notably for Big Sur full-screen where the hypersearch panel becomes a separate maximized window;

revert 1105c42722dc on isabelle-release branch;

proper hostname;

more official support for macOS 11.1 Big Sur;

more informative error; tuned;

added lemmas

merged

updated to scala-2.13: its ArraySeq implementation is not usable here (requires scala.relection.ClassTag);

updated to scala-2.13.4;

clarified;

clarified return code: re-use SIGALRM for soft timeout;

clarified signature: more operations;

tuned;

clarified signature: support more generic server implementations;

tuned comments;

proper </html>;

tuned message;

new magerial from Jakub Kądziołka

back to post-release mode;

Added tag Isabelle2021-RC2 for changeset 802647edfe7b

tuned;

avoid Unicode quotes;

clarified pretty margin: attempt to avoid scrollbar;

more documentation;

more informative errors: simplify diagnosis of spurious failures reported by users;

proper labels for status message: "sidekick.parsing-complete={0} parsing complete, {1} error(s)";

proper size of buttons in Symbols dockable, e.g. \<A> 0x01d49c vs. \<B> 0x00212c;

clarified list of presented look-and-feels; clarified signature;

clarified default L&F of Isabelle/Scala (not Isabelle/jEdit);

discontinued odd absolute position (amending 85bcdd05c6d0, 1975f397eabb): it violates translation invariance of commands and may lead to redundant re-checking of PIDE document;

Corrected lemma that was too specific in HOL-Computational_Algebra

tuned GUI, notably for scalable FlatLaf;

clarified default L&F;

support for additional look-and-feels;

avoid rescaled fonts, e.g. dockable buttons on Windows L&F after opening a new view;

some algebra material for HOL: characteristic of a ring, algebraic integers

HOL-Data_Structures: added Selection and time functions for list functions

merged

discontinued body_range (again): does not quite work, because Position.thread_data is plain Toplevel.pos_of only;

clarified: command keyword position is sufficient (amending 693a39f2cddc);

ignore error messages produced by CVC4 when generating BV

One useful lemma/simprule

isabelle update_cartouches;

tuned --- prefer explicit position;

recovered body_range from eca176f773e0 --- its Command.core_range is in conflict with batch-build markup;

tuned;

support more command positions, analogous to Command.core_range in Isabelle/Scala;

tuned;

more uniform core_range (amending def3ec9cdb7e);

clarified dock icon: setup earlier on startup;

clarified NEWS;

dropped junk

try GTK 3: some visual dropouts, but more stable e.g. in Sidekick "isabelle-markup";

detect arm64-darwin more reliably: uname could be in x86_64 mode, e.g. within app bundle;

proper purge for arm64-darwin;

updated jdk-15.0.1+9, including arm64-darwin;

discontinued somethat pointless sharing: too complicated;

less verbose;

more robust sharing, despite minimal impact on archive size;

proper LSMinimumSystemVersion for zulu-jdk-15;

obsolete, thanks to zulu-jdk directory layout;

clarified Info.plist;

more direct ISABELLE_JDK_HOME, thanks to zulu-jdk directory layout;

prefer OpenJDK from Azul: supports more versions and platforms; support arm64-darwin;

sort lines;

tuned;

more NEWS;

recovered file-type icons from macos_app;

clarified application init;

recovered bundle icons (not application) from macos_app;

proper app directory setup, without macos_app component;

more robust;

prefer official Java 9 operations;

obsolete;

proper dock icon for macOS;

proper isabelle_home_prefix; proper isabelle_options, with link;

discontinued macOS JavaAppLauncher: re-use plain shell script; more uniform java_options for all platforms;

tuned whitespace;

tuned -- generate Info.plist in Isabelle/Scala;

tuned signature;

tuned signature;

updated according to ~~/etc/settings; tuned;

more portable component setup;

clarified quotes;

tuned -- generate script by Isabelle/Scala;

proper treatment of XML.Wrapped_Elem, e.g. Markup.class_parameter;

proper theory name, e.g. for HTML/PIDE presentation;

more robust and permissive;

present theory using PIDE markup;

clarified signature;

tuned signature;

tuned

HOL-Library.Multiset: new notation for prod_mset, consistent with sum_mset

merged

more documentation;

override existing action, to retain menu item;

HOL-Complex_Analysis: coefficient asymptotics for meromorphic functions

HOL-Library: Changed notation for sum_mset

tuned;

proper thread position for reports;

tuned signature;

misc tuning and clarification;

tuned signature;

tuned;

alternative shortcut, notably for macOS;

action isabelle.toggle-full-screen;

some attempts at multi-platform full-screen mode;

more operations;

clarified HTML presentation elements;

more robust bootstrap: Isabelle-jEdit.shasum could be absent;

tuned whitespace (amending a4bffc0de967);

clarified caching;

persistent hash code: much faster caching;

clarified signature: absorb XZ.Cache into XML.Cache;

support more direct hash-consing via XML.Cache;

tuned;

tuned signature;

clarified boundary case;

more uniform default --- hardly relevant in practice;

proper ssh_port (amending ffd8283b7be0);

clarified signature --- internal Cache.none;

tuned comments;

more verbosity for potentially bulky presentation;

tuned signature -- prefer Isabelle/ML structure Integer (despite minor confusion due to canonical argument order of "pow");

tuned signature -- prefer Isabelle/ML structure Integer;

tuned signature -- prefer Isabelle/ML structure Integer;

more lemmas

added lemmas

added lemma

tuned whitespace;

Added tag Isabelle2021-RC1 for changeset d4b67dc6f4eb

updated for release;

clarified HTML presentation, e.g. avoid bulky jobs like HOL or HOL-Analysis in applications;

follow Phabricator update 2020 Week 42;

updated for release;

tuned;

proper NEWS according to current situation;

updated for release;

tuned (see also b5333fc056da);

A few more simprules for iff-reasoning

infinite products iff simprule

merged

merged

Two biconditional simprules for summable

updated to sqlite-jdbc-3.34.0, with support for native arm64-darwin;

support ISABELLE_APPLE_PLATFORM64 (Apple Silicon);

more robust: clarified error when merging Hoare_Logic + Hoare_Logic_Abort;

more robust components_base: avoid fragile directory links on Windows (or Cygwin);

more NEWS;

merged

avoid memory problems on test machine;

more robust defaults: spurious problems with parallel invocations and interrupts;

more interrupts;

avoid multiple uses of the same ML file;

tuned document, notably authors and sections;

clarified presentation of files for each theory;

disable auto_nitpick for now: spurious problems with non-termination e.g. in HOL-Hoare examples;

clarified modules: avoid multiple uses of the same ML file; clarified concrete vs. abstract syntax;

clarified session: avoid merge of different syntax from different Hoare logics;

clarified modules: avoid multiple uses of the same ML file;

clarified syntax modes, avoid obsolete "xsymbols";

clarified fonts, notably for Windows L&F;

support jdk-15;