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

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).

minor clean up under examples/machine-code

Remove trailing whitespace in source files.

Minor tweaks.

Minor changes.

I've changed the way tail-recursive functions are defined.
They are now defined based on a step function:

step: 'a -> 'a + 'b

Tail-recursive functions loop until their step function
returns something in the right component (INR).

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!

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.

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