added Mirabelle option -r to randomize the goals before selection

Removal of a lemma (now in the libraries) and a few tweaks

A new lemma about inverse image

proper treatment of $let variables in symbol table in Sledgehammer

The parent of "../.." is "../../.." not "..". Fixes #167.

Try using the atomic operations added in ARM 8.1. These are not available in…

Change to use load-acquire to lock and swap-release to unlock.

Restore the spinning that was previously used to check for a mutex lock.

Disable LSE atomics for the moment.

Allow for the extremely unlikely situation of floating point constants in a…

Don't include container arguments among the "stable" arguments for non-tail…

Sort the constant lists to avoid duplicates. Use bit-encoding for 64-bit…

Use movi for floating point zero.

Fix float constants for big-endian.

Implement floating point constants in the non-address area.

Remove CheckRTSException; add back CPUPause.

Added load/storePolyWord/NativeWord functions to RunCall.

Use TBZ/TBNZ for tag test and branches.

Move code to check for RTS exceptions into the RTS caller for the X86. This…

Combine adjacent pushes, combine stack resets and use post-indexing to include…

Use ldp and stp for adjacent loads and stores where possible.

Begin peep-hole optimisation. Eliminate unnecessary branches and straighten…

Handle allocations of > 4096 which was omitted in earlier change.

Move allocation code and branch tables into pre-assembler "instructions".

Convert ForeignCall to use the pre-assembler layer. Remove ArmSequences and…

Remove temporary functions that converted the pre-assembly code to the assembly…

Return small numbers of multiple results in registers.

Fix another case where the optimiser added a new tuple but didn't set the…

Clean up the conflict test for arguments of long format arbitrary precision…

Support for multiple results from function calls.

Don't attempt to merge cache states for the moment. It seems to be broken.

Fix the optimiser so that it sets the correct argument type for newly…

Use hints to improve the chances that we will be able to retain cache states…

Add a dummy instruction if we're caching to see if this is the problem.

Fix incorrect test.

Use an indexed load in 32-in-64 if the offset is zero and this is the last…

Merge the cache state on multiple paths.

Include the cache registers in the save mask for allocations so that if there…

Change the assertion into a test and don't optimise if the result of the load…

Cache the combination of loading a value from the stack and getting the…