less ambitious parallelism: more direct read/write saves overall heap space and GC time;

slightly faster XML output: avoid too much regrowing of StringBuilder;

updated NEWS: arm64-linux support is almost complete;

update z3-4.4.0pre-3 to z3-4.4.1, which happens to have an arm64_linux executable in Debian 9;

more material for HOL-Analysis.Infinite_Sum

more symbolic latex_output via XML;

clarified signature;

updated to polyml-5.9-610a153b941d -- close to final;

tuned signature (again): latex_output is likely to depend on context;

more symbolic latex output; discontinued Latex.output_text, which is in conflict with symbolic output;

tuned signature;

symbolic latex_output via XML, interpreted in Isabelle/Scala;

tuned signature;

clarified signature;

clarified signature;

clarified signature: more privacy;

tuned output --- less redundancy;

tuned whitespace;

clarified signature: Latex.Output as parameter to Document_Build.Engine; tuned;

proper detection of ARM platform variants;

back to post-release mode;

updated for release;

Added tag Isabelle2021-1-RC3 for changeset 2b212c8138a5

merged

updated to polyml-5.9-cc80e2b43c38, which also contains ARM64 on darwin (unused by default);

clarified HTML_Context: more explicit directory structure;

tuned comments;

tuned;

clarified signature;

clarified properties: avoid empty entry;

tuned signature;

merged

tuned (thanks to J. Villadsen)

added padding to Mirabelle's output

merged

tuned generation of TPTP with $ite/$let in higher-order logics

tuned generation of TPTP with $ite in function position

tuned TPTP generation of If helper facts

merged

clarified signature: prefer static operations;

clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources;

more robust;

tuned signature;

clarified signature: more explicit class Entity_Context with private state + operations;

more hyperlinks, notably internal fact references;

Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.14UUXO

A tiny bit of tidying connected with Zorn's Lemma

tuned;

tuned;

proper handling of Protocol.Export, using the payload from the message --- in contrast db_context.read_export materializes only later by a different thread (race condition);

revert temporary workaround 6d111935299c;

added lemma

merged

tuned attributes to avoid looping

added eq_iff_swap for creating symmetric variants of thms; applied it in List.

tuned text;

more robust timeout, following df4449c6eff1;

more accurate Files.isRegularFile, exclude directories (e.g. jar_path);

proper java_version for isabelle_setup;

explicit option metric_argo_timeout, with reasonable default for Raspberry Pi;