tuned;

tuned;

clarified order: accumulate strictly from left to right;

clarified modules;

clarified modules;

tuned signature;

clarified signature: more types and operations;

clarified signature;

tuned;

proper file extension for Isabelle_System.extract;

tuned implementation;

more uniform use of make_directory;

tuned message;

tuned: less redundant implementation;

clarified signature: copy directory content more directly;

more robust;

tuned whitespace;

clarified signature: more general operations;

clarified signature;

tuned signature;

tuned signature;

clarified signature;

tuned;

merged

Strengthened multiset lemmas w.r.t. irrefl and irreflp

clarified signature: proper scopes and types;

maintain global state of document editor views, notably for is_active operation;

tuned signature;

tuned whitespace;

clarified modules;

clarified signature: more robust;

tuned;

clarified modules;

more specific GUI for document nodes;

tuned;

tuned;

tuned;

tuned;

tuned;

tuned;

tuned;

merged

clarified signature: just one level of arguments to avoid type-inference problems;

tuned signature: more operations;

tuned;

clarified signature;

stated goals of some lemmas explicitely to prevent silent changes

rewrite proofs using to_pred attribute on existing lemmas

clarified signature: less redundancy;

tuned;

potentially more robust delay_load action: avoid loosing events due to guards;

tuned signature;

tuned;

tuned signature;

more uniform tooltip for plugin options dialog;

tuned signature;

tuned signature;

more uniform session selectors, with persistent options;

tuned;

NEWS

merged

added lemmas asym_if_irrefl_and_trans and asymp_if_irreflp_and_transp

added lemma totalp_on_converse[simp]

added lemmas irrefl_on_converse[simp] and irreflp_on_converse[simp]

added type annotations and tuned formatting

strengthened and renamed irreflp_greater[simp] and irreflp_less[simp]

merged

tuned GUI behaviour;

more GUI elements;

clarified modules;

clarified process: implicit load() when finished;

more robust, notably initial update();

tuned;

tuned messages: implement "verbose = false", but there is no theory output anyway;

merged

added lemmas irrefl_on_subset and irreflp_on_subset

introduced predicates irrefl_on and irreflp_on, and redefined irrefl and irreflp as abbreviations

tuned messages;

tuned message;

tuned messages and options;

merged

removed prod_set_conv attribute from top_empty_eq and top_empty_eq2

discontinued "unzip" executable (see also eb96243a25c5 and 662de910a96b);

more direct access to jEdit jar resources, without unzip;

clarified check: allow to remove bad directories;

clarified check; tuned message;

tuned message;

tuned signature;

tuned signature;

proper unzip with strip option, within the JVM; tuned component build process;

updated to sqlite-jdbc-3.39.4.1; clarified directory layout;

more standard component build process;

clarified signature: prefer Scala functions instead of shell scripts;

tuned;

more direct target directory;

clarified signature: prefer Scala functions instead of shell scripts;

A new Isabelle/CTT example, and eliminated some old-style quotation marks

clarified exception: avoid odd compiler warning;

update to scala-3.2.1; enforce rebuild of Isabelle/ML + Isabelle/Scala;

recovered check from 69139cc01ba1: Windows does not support PosixFilePermission;

update to jdk-17.0.5 (Oct-2022);

more standard component build process;

proper treatment of tar.gz double-extension;

proper download, instead of assuming local directory;

more standard component build process;

clarified signature; omit somewhat pointless test for "unzip" command;

clarified signature; tuned messages;

discontinue unused JCEF: superseded by Electron with its bundled Chromium;

prefer deterministic result;

clarified command-line arguments: follow more recent isabelle build_XYZ;

compile

correctly show '(> 2 s, timed out)' or similar in Sledgehammer's output

merged

strengthened and renamed lemma reflp_on_equality

renamed lemmas linorder.totalp_on_(ge|greater|le|less) and preorder.reflp_(ge|le)

Added an example for Isabelle/CTT

clarified signature;

clarified signature: more explicit types;

tuned output;

prefer sorted result;