Added contributors

clarified basic Linux packages;

merged

type class reduction

merged

de-applying and tidying

guide continued

factored out theory Bits_Int

early and more complete setup of tools

factored out theory Bits_Int

factored out singular operation into separate theory

reactivate veriT after changing options in 11f645d25498

renamed constant

improved proofs

merged

discontinued old platforms;

merged

tuned proofs

nice new version without even/odd case splits

remove unsupported max-time option from veriT calls

more standard Value.print_time;

disable verit-2020.10-rmx-1 for now: does not quite work on Windows and macOS;

proper support for Windows exe;

proper Isabelle component settings: prefer standard terminology…

provide verit-2020.10-rmx for testing (inactive);

proper setup for Windows/MinGW;

proper libraries_closure for libgmp;

tuned;

updated to polyml-test-d68c6736402e --- follow current ongoing development;

localized example to avoid name clashes

tuned names

The general "tail" instruction is now in the extended set.

merged

tuned names

Fix offsets in test.

genRTSCallFastGeneraltoFloat is now an extended operation.

LoadC8/StoreC8 use genCAddress so that involves an extra item on the stack.

LoadC8/StoreC8 now take both an offset and an index as with the other C-memory…

Don't build the UnixSock structure on Windows.

update build script for veriT 2020.10-rmx

merged

more robust;

proper target directory for libraries;

proper library names on Windows;

build Isabelle Zipperposition component from OPAM repository;

proper support for Windows/Cygwin: "zipperposition" vs. "zipperposition.exe";

tuned messages --- less SPAM;

tuned;

tuned signature;

misc tuning and clarification: prefer Executable.libraries_closure;

tuned;

more portable;

reconstruction of veriT proofs in NEWS

Revert accidental inclusion of project file in last commit.

Fix K and E exports for 32-in-64.

PE/COFF exporter: Save the first relocation and write it to the end of the…

Move one opcode value because the value was still being used during the…

Remove the intermediate stage instructions and add a couple of reduced…

Combine jump with equalLocalB.

Combine the tag check instructions with jumps.

Move some more rarely used instructions into the escaped instruction group.

Replace a conditional branch round an unconditional branch by a conditional…

Link branches together to avoid a branch to a branch.

Add an optimisation pass. Currently this only deals with eliminating…

Add some combined instructions that implement common sequences for datatype tag…

Improvements to interpreted code and the interpreter. Add code to handle…

Fix bug that only showed up after several bootstraps.

Fix bug in indexed case in the interpreter. Start adding composite…

Overhaul the interpreted code. Separate rarely used instructions into two-byte…

Add separate descriptors for entry points and weak references. These are…

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

Add hint file for Visual Studio.

Change DEBUGGER signature in ROOT file for interpreted version

add reconstruction for the SMT solver veriT

Add well-foundedness of trivial unit relation

NEWS;

activate E 2.5 for production use (see also 5d1a7b688f6d);

clarified signature;

clarified Executable.libraries_closure;

dedicated module for toplevel target handling

consolidated names and operations

replaced combinators by more conventional nesting pattern

avoid _cmd suffix where no Isar command is involved

centralized case distinction for beginning and ending nested targets in one…

adjusted to changes in distribution

replaced combinators by more conventional nesting pattern

consolidated names and operations

support for platform-specific executables;

removal of a synonym

merged

merged

tidying and removal of legacy name

tuned whitespace;

more robust: ignore existing gmp installation, but let veriT incorporate…

presumably redundant (absent in Windows/Cygwin download);

clarified signature;

tuned messages;

build Isabelle veriT component from official download;

tuned;

tuned messages;