Merge

reverted simprule status on a new lemma

merged

tiny bit of lemma hacking

tuned --- fewer warnings;

tuned --- fewer warnings;

tuned --- avoid deprecated conversions between certain number type;

tuned --- avoid deprecated Predef.any2stringadd;

tuned --- silence odd warning;

tuned --- fewer warnings;

tuned --- fewer warnings;

tuned --- fewer warnings;

tuned --- fewer warnings;

clarified signature, according to Isabelle/Scala;

download more directly, via means of JVM;

download on separate thread;

clarified signature;

tuned;

proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.);

tuned signature;

NEWS

lemma diffusion

more connections between mset _ = mset _ and permutations

dissolve theory with duplicated name from afp

more robust (amending 87403fde8cc3): notably allow symlink to existing directory, which Files.createDirectories does not accept;

more Isabelle/ML/Scala operations;

more Isabelle/ML/Scala operations;

more Isabelle/ML/Scala operations; clarified errors;

proper src1, amending 20157c8ab3f3;

tuned;

proper File.eq, amending df49ca5da9d0;

tuned;

clarified modules: more like ML;

obsolete;

tuned;

more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552);

discontinued somewhat pointless "integrity test of build_history": it fails right now, but also failed to expose spurious incompatibilities when it was working;

more checks;

clarified message;

clarified message;

clarified comments;

clarified message;

improved list_neq simproc

merged

repaired document

merged

merged

A couple of basic lemmas about arg

multiset as equivalence class of permuted lists

emphasize connection to multisets

proper "latest" tag, otherwise the default pull command from https://hub.docker.com/r/makarius/isabelle won't work;

more on Isabelle_System.bash;

more specific name

more lemmas

dropped obscure FIXME

proper usage of hypotheses for zipperposition's TPTP generation

merged

tuned Mirabelle to parse option check_trivial only once

merged

merged

added stride option to Mirabelle

proper prover capabilities for zipperposition

NEWS;

merged

clarified uses of Isabelle_System.bash_process: more checks, fewer messages;

tuned signature;

more direct timing from bash_process wrapper;

tuned;

clarified signature, following Isabelle/Scala;

tuned;

clarified signature;

clarified signature: Isabelle_System.bash_process is strict and thus cannot check for interrupt_return_code;

clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;

tuned;

clarified signature, following Isabelle/Scala;

tuned signature;

clarified signature: process_result timing from Isabelle/Scala;

NEWS

dedicated locale for preorder and abstract bdd operation

get rid of traditional predicate

proper treatment of process_result;

more accurate process_result in ML, corresponding to Process_Result in Scala;

clarified: proper trim_line for error;

unused;

clarified lines (again);

clarified modules;

more uniform Bash.process: always ask Isabelle/Scala;

more reactive protocol messages, e.g. for Scala.function (relevant for Bash.process);

clarified compiler options;

tuned comments;

removed obsolete RC tags;

more hints;

merged

Added tag Isabelle2021 for changeset 7e2a9a8c2b85

provide naproche-755224402e36;

provide naproche-4ad61140062f;

HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.

tidied up a few ugly proofs

merged

provide naproche-6d0d76ce2f2a;

Added tag Isabelle2021-RC6 for changeset ed36e33a2e4b

updated to flatlaf-1.0;

tuned NEWS;

tuned comments;

more robust interrupt handling as in Future.forked_results (amending 64df1e514005);

more parallelism: avoid exhaustion of standard thread pool;

more robust: resolve historic components via current tool to access current server;

tuned signature;

more parallelism;

more robust ISABELLE_COMPONENT_REPOSITORY: use current value of managing process to avoid its fluctuation in ancient history;

clarified signature;

merged;

Added tag Isabelle2021-RC5 for changeset a88dbf2a020f

provide naproche-7d0947a91dd5;

more complete solutions (amending 4d36070bdbf4);

terminate faster (following dd9fc8a3036c);

more robust: accommodate output lines produced by Scala "bash_process";

updated for release;

updated to flatlaf-1.0-rc3;

more robust: allow YXML text;

inherit ISABELLE_TMP from ML process, e.g. required for $AFP/Hello_World/RunningCodeFromIsabelle.thy;

support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;

clarified modules: less redundancy;

clarified modules: allow early invocation of Scala functions;

clarified modules: allow early definition of protocol commands;

clarified links to external files, e.g. .pdf within .thy source document;

avoid interference with FlatLaf fonts, see also jEdit SVN 24885 'Updated Appearance option pane to allow setting "primary" and "secondary" fonts for all look and feels.' (daleanson 2018-08-30);

updated to flatlaf-1.0-rc2;

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;