Avoid some "inventing new type variable" messages.

Fix some machine-code code for the new by

Fix some machine-code theories for pat_assum rename

Add Theory.quote_adjoin_to_theory. Use this in llistTheory.

This should close #304.

This has been implemented using a new function Portable.quote_to_string_list. Other uses of adjoin_to_theory under src/ have been updated.

slightly improved support for SPEC_1

Guard against some parsing problems.

bug fix for SEP_R_TAC

SEP_R_TAC improved

Support for generating TEMPORAL triples.

Currently works for ARM, M0 and MIPS models. Yet to update the x86-64 model.

another bug fix in SPEC_COMPOSE_RULE

Various updates/improvements to the decompiler tools.

bug fix for SPEC_COMPOSE_RULE

Minor improvements to ARM tools.

Update M0 tools.

Minor updates to other ISA tools.

Updates and improvements to the l3-machine-code decompilation tools.

Further updates to the tools linking the L3 ARM model to the decompiler.

A lot of code has been generalised (making it usable with other models) and the performance has been improved.

Update to ARM tools.

Triples are now generated with a "mode" variable. This is required to satisfy the "GoodMode" predicate. Before concrete modes were used, e.g. "16" for user mode.

In addition, various performance related enhancements have been made in helperLib (especially with regard to AC rewriting for the "*" operator).

Attempt to make term parsing in x64_decompLib more stable.

minor clean up under examples/machine-code

bug fix

removing 'prove' from some automation

Fixed automation that broke due to 632a78

Also did some other tidying up.

Remove some trailing whitespace.

Various minor changes.

Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.

Remove trailing whitespace in source files.

Minor tweaks.

Many minor additions/changes.

Hoare triples for 64-bit x86 and some tweaks in other places.

Fix.

Minor tweaks.

Minor changes.

Multiple minor changes.

Minor update.

A few bugs fixed.

Minor update.

A general update.

Many minor changes.

Many minor updates.

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

A general update:
1. the decompiler is now slightly faster, due to new code
abbreviations (terms smaller in internal proofs);
2. the definition of the machine-code Hoare triple
was slightly altered to support instruction caches;
3. the x86 model now includes an instruction cache.

Also, I give up on attempting to support MoscowML for
examples/machine-code/lisp. Both the standard kernel and the
experimental kernel crash while loading files in this
directory using the latest patched version of MoscowML.
Both kernels exit with an uninformative message:

Compiling lisp_equalScript.sml
Linking lisp_equalScript.uo to produce theory-builder executable
Uncaught exception: Chr
Failed to build script file, lisp_equalScript

Did they run out of memory? If so, why does the error message not
say so?

Pulled across change 6835 from the release branch so that this code
can compile with Moscow ML.

A general update. Now lisp_finalTheory produces assembly files
containing the verified LISP interpeteres (in machine code):

arm_eval.s
x86_eval.s
ppc_eval.s

Each of these have been successfully run on real hardware, for
each respective platform.

The proof scripts are likely to only work in the experimental
kernel, due to some unfortuante differences between the two
kernels. Some of these differences are exposed more frequently
now due to recent(ish) changes to the datatype package. Maybe
some of the changes made to the datatype package ought to be
reconsidered?

Various minor modifications, also added two files
that were apparently missing from the svn version.

Restructuring and simplification.

Improvements to the verified LISP interepreters.

The new interpreters have been proved to implement
McCarthy's LISP 1.5 as formalise by Mike Gordon
for the ACL2 workshop 2007.

Warning: lisp_evalScript takes 73 minutes to run
using Holmake under PolyML.

Updates requested by Lu Zhao.

A new version of files previously in examples/mc-logic.
Eventually examples/mc-logic will be deleted.