separation of reversed bit lists from other material

separation of reversed bit lists from other material

merged

avoid exhaustion of worker threads, notably due to complex interaction of…

more robust: insist in finished future;

unused;

further refinement of code equations for mask operation

further refinement of code equations for mask operation

uniform mask operation

clearer separation of pre-word bit list material

uniform mask operation

clearer separation of pre-word bit list material

repaired document slip

added lemma

more consequent transferability

more consequent transferability

Update compiler version to 5.8.2 so that we pick up the correct files on…

Check inside the simplifier that the body of a potential inline function is…

Remove unused parameters.

Merge branch 'master' of github.com:dcjm/polyml

Search for machine/reloc.h separately from elf_abi.h. These seem to have been…

Change all the casts from PolyWord* to stackItem*. Some had been missed.

more robust scheduler shutdown, notably for spurious crashes;

unclear why I ever asked for type tree2

enforce pide_session to see if all isabelle_cronjob tasks work smoothly with it;

proper pretty printing for latex output, notably for pide_session=true…

clarified name to avoid duplication (no distinction of data on host =…

clarified names;

more errors;

much faster proofs (cf. Isabelle/bad75618fb82);

follow Phabricator update 2020 Week 27;

tuned;

Fixed failing proofs.

unused;

clarified errors: avoid hiding of import_errors/dir_errors by their…

clarified signature;

clarified errors: avoid accidental import from other session that happens to be…

clarified order --- proper sorting of requirements;

obsolete (see 9cde8c4ea5a5);

tuned --- based on hints by IntelliJ;

tuned signature;

Mostly improving theory format (adding line breaks) and added

Added proofs about get_tag_type.

Remove push and pop of rcx/ecx in CALL_EXTRA macro. This seems to be a relic…

Merge commit '196ac3bc7d11b43f488fb945077aac162144bd31'

Move the test for the result of PolyCompareArbitrary up to the top-level of…

Add PointerEq as a binary operation and reserve WordComparison for the tagged…

updated to polyml-5.8.1 (official release);

Merge branch 'master' into GCPercent

Add Unix socket test. This was added in another branch.

subtle change of Theory_Data extend/merge semantics due to Theory.join_theory;

Added Weak.touch to Weak structure documentation.

data extend is obsolete and should be identity;

Updated pre-built compilers for 64-bit amd 32-in-64 Windows.

Rebuild pre-built compilers for 64-bit SysV, 32-in-64 SysV and 64-bit…

Updated pre-built compilers for 32-bit native X86 and interpreted versions.

Rebuild configure with new release numbers.

Update version numbers ready for release of 5.8.1.

clarified -- avoid non-standard extend/merge;

clarified -- avoid non-standard extend/merge;

tuned -- avoid non-standard extend;

proper session imports;

clarified -- avoid non-standard extend;

tuned -- avoid non-standard extend/merge;

prefer conservative extend/merge of theory naming;

support native PID for ML process;

merged

proper import sessions;

more thorough extend/merge (for Theory.join_theory);

clarified theory data: more robust merge;

more thorough extend/merge, notably for master_dir across Theory.join_theory (e.

more robust: avoid potential problems with encoding of directory name;

more thorough extend/merge (for Theory.join_theory);

more thorough extend/merge (for Theory.join_theory);

tuned grouping

yet another alias

more robust wrt. experimental changes in Poly/ML;

more robust: handle unavailable statistics;

merged

clarified user counters: expose tasks to external monitor;

proper platform path for Windows;

clarified signature;

support for monitoring of external ML process;

clarified signature;

more robust;

support for monitoring of external ML process;

clarified modules: ML_Statistics within bootstrap environment;

misc tuning and modernization;

clarified examples;

Add a related check for offsets that could exceed a signed 32-bit value.

Short constant index values can be put into the offset but leave larger and…

Modify test so that it works if int is IntInf.int.

merge from afp-2020

update maintenance docs

concatentation of bit values

concatentation of bit values

saturation framework: renamings

prefer canonically oriented lists of bits and more direct characterizations in…