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…