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