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;

more friendly desktop application on macOS;

default simprule for geometric series

tuned

less aggressive auto-build: avoid change of running jar;

clarified window size;

more robust Java monitor: avoid odd warning about insecure connection;

tuned signature;

clarified modules;

clarified modules;

misc tuning for release;

rebuild component with proper ZIPPERPOSITION_HOME for sledgehammer;

sort lines;

provide zipperposition-2.0 for experimentation;

merged

tweaked tptp parsing when source info is missing

tuned comments;

merged

proper relative path;

unused;

present auxiliary files with PIDE markup; more robust treatment of non-text files (notably $POLYML_EXE);

tuned;

tuned;

tuned signature: more explicit types;

tuned signature;

clarified signature and module structure;

tuned signature;

clarified comments: file-system access is always unsynchronized;

more precise simpset for method unat_arith

clarified scope of concept

clarified name

tuned;

download auxiliary files via "curl";

clarified markup: open URL as editor file;

download as in Isabelle/Scala;

more robust;

improved markup for theory header imports;

clarified markup (refining dd56ba1974e6);

more documentation;

merged

tuned running time functions

merged

proper support for Windows/Cygwin;

updated to zipperposition-2.0 and ocaml-4.07, which is required for it;

more checks;

merged

simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)

added missing +1 to T_insert (for function call)

merged

afford more reactive input;

more NEWS;

more documentation;

added action isabelle.goto-entity to follow links in a narrow formal sense;

tuned signature;

clarified select_entity (again): it is meant as approximation to "refactoring" and thus only makes sense for defs within the same buffer;

clarified caret focus modifier, depending on option "jedit_focus_modifier";

tuned;

tuned;

enabled FOOL for E

merged

tuned name generation in tptp to not depend on shadowing

tuned lambda translation for fool

generate unique variable names in tptp

proper handling of true and false in tptp

proper eta-expansion to avoid lambdas in tptp fool

proper proxification for fool + refactoring

proper renaming of THF_Lambda_Bool_Free

proper parsing of type encoding; tuned naming

proper handling of builtins in TFX

proper generation of TPTP output for higher order builtins

tuned

merged

removed redundant T_xxx_bound_aux lemmas

don't generate not-fully-defined bit-vector constants in SMT problems

improve and activate compression for veriT proof reconstruction

unused (see 29566b6810f7);

proper argument --- amending 908d8be90533;

tuned;

tuned signature;

tuned signature;