updated to polyml-5.8.2 (official release);

clarified default_platform_families (again);

proper option for linux_arm;

proper "$?";

proper jvm_platform, notably for org.sqlite.lib.path;

tuned message;

support for platform family "linux_arm";

clarified purge;

removed junk;

support local build_heaps; more robust build_release;

merged

tuned --- rename = dist_name is sufficient;

proper dist_name;

clarified option -P: allow empty argument;

support for existing release archive; misc tuning and clarification;

tuned signature;

clarified signature;

more website content;

misc tuning and clarification: more explicit types Release_Context, Release_Archive;

tuned signature;

tuned theory structure

more appropriate location

collected lemmas on permutations

A nice cardinality lemma

tuned

more robust indentation: proper line context after insert;

more robust: avoid sporadic crash of JEditBuffer.tokenMarker.getMainRuleSet().getModeName();

support nested cases;

tuned;

tuned;

early definition of ML antiquotations;

tuned;

clarified signature: more operations;

clarified signature: more operations;

clarified signature;

tuned signature;

clarified command-line, following other build_XYZ tools;

more recent OCaml and GHC stack: better support for Apple Silicon;

merged

avoid "exec" to change the winpid;

clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);

fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);

clarified signature;

rebuild executable for x86_64-darwin;

clarified command-line;

update Linux base-line;

tuned comments;

tuned signature;

simplified typesetting of \<guillemotleft>...\<guillemotright>;

collecting more lemmas concerning multisets

proper use of antiquotations;

more documentation on "Conversions";

tuned

updated example;

clarified options (again);

more options: update ISABELLE_IDENTIFIER;

clarified conditional ML;

support for conditional ML text;

updated example;

clarified options;

proper context variable handling when stripping leadings quantifiers from test goals

proper etc/ISABELLE_ID from archive (amending 4cba4e250c28);

eliminated perl: prefer elementary GNU printenv;

more robust bootstrap of components;

more self-contained support for macOS;

misc tuning and clarification;

tuned signature;

support for base64 via Isabelle/Scala/ML;

compile;

clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);

clarified signature (again);

merged

clarified signature;

unused;

unused;

clarified signature: more structured arguments, notably for remote provers;

clarified signature;

clarified signature: avoid tmp file;

clarified signature for Scala functions;

clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9);

tuned;

clarified cache;

clarified signature: Bytes extends CharSequence already (see d201996f72a8);

clarified exceptions;

more uniform use of Byte_Message; support protocol_message with multiple chunks;

tuned signature;

tuned signature;

more robust treatment of empty markup: it allows to produce formal chunks;

collected combinatorial material

tuned;

tuned;

more documentation;

proper treatment of nested antiquotations; clarified signature;

support for ML special forms: modified evaluation similar to Scheme;

clarified signature: more detailed token positions for antiquotations;

merged