update to gmp-6.2.1, with support for arm64-darwin;

clarified platforms;

clarified options: implicitly support both x86_64 and arm64;

tuned whitespace;

centralized more lemmas

avoid Fun.swap

guide is out of focus

avoid Fun.swap

centralized more lemmas

guide is out of focus

proper build for fresh target directory (amending d9823224fcfe);

put more resources into jedit_build component;

more brackets (see f6b453449cc6);

more brackets;

proper settings variable, amending 6e85281177df;

merged

tuned proofs --- avoid z3, which is absent on arm64-linux;

proper condition: z3 could be absent, e.g. on arm64-linux;

build auxiliary jEdit component in Isabelle/Scala;

tuned message;

separate component for idea-icons.jar, from jedit_build (see also ff0e0bb81597);

clarified signature;

tuned signature;

Relational_Minimum_Spanning_Trees: refactoring Boruvka.thy

more elementary swap

more elementary swap

Handle re-exporting code with ADRP/LDR sequence.

tuned comments;

misc updates and clarification;

clarified file name;

merged

slight tidying of 1.19

updated to polyml-5.8.2 (official release);

merged

proper option for linux_arm;

clarified default_platform_families (again);

Rebuilt after merge.

Merge branch 'master' into ARMMerge2

proper "$?";

Rebuilt pre-built compiler with endian fix.

Merge branch 'Endian5.8.2' into fixes-5.8.2. Fixes #150

Only call PolyIsBigEndian when the code segment is being created. It was…

Remove 5.8.1 compatibility files.

tuned message;

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

clarified purge;

support for platform family "linux_arm";

support local build_heaps;

removed junk;

no hardwired document;

merged

tuned --- rename = dist_name is sufficient;

proper dist_name;

clarified option -P: allow empty argument;

support for existing release archive;

tuned signature;

more website content;

clarified signature;

tuned signature;

misc tuning and clarification: more explicit types Release_Context…

tuned theory structure

more appropriate location

tuned theory structure

more proof tidying

merged

collected lemmas on permutations

collected lemmas on permutations

merged

simpler proofs of stronger lemmas

just a few more tweaks

Pre-built compilers for X86/64 Windows and X86/64-32 Windows.

Fix 32-bit pre-built compilers wrongly built.

Built pre-built compilers for X86/32 and 32-bit interpreted.

Rebuilt compilers for SYSV X86/64, X86/64-32 and 64-bit interpreted.

Rebuilt confure for new release.

Update version numbers ready for release of 5.8.2

Tweaks

restructure proof

A nice cardinality lemma

tuned proofs

renamings

tuned

lemma poly_asymp_equiv + simplified existing proof based on this lemma

more robust indentation: proper line context after insert;

support nested cases;

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

tuned;

tuned;

early definition of ML antiquotations;

tuned;

merged

some revisions to Lemma 3.7

Formatting, remove wrongly added file

small refinements to partition proofs

merged

Add imperative deletion operation and OCaml code export to BTree entry

cleaning proofs, use more real_asymp

clarified signature: more operations;

clarified signature: more operations;

tiny bits of tidying up / simplification of proofs, aided by new lemmas