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;