Remove TABs from examples

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!

Fix for a Define bug spotted by mjcg. When
dealing with recursive calls under a case,
if variables with certain names (those
starting with v) are bound in the case
pattern then it can happen that variables
generated during pattern matching can be
the same, leading to failed proofs. Totally
obscure, and dealt with properly (I think)
in normal pattern matching. So, a difference
between Pmatch and Functional. The fix is
to invent a class of variables not accepted
by the parser (i.e. starting *v) and to later eliminate
the weird names from any theorems coming out of Hol_defn.

Some other trivial mods made in passing also, plus
tests for the new behaviour.

Also a new conversional, MAP_THM, which applies the
given conversion to the assumptions and conclusion
of the given theorem.

Fixed LLEQ_THM to work in both kernels.
Replaced store_definition with save_thm.

Modifications to ensure the files work under the experimental kernel.

Fixed various proof scripts in acl2_packageScript.sml and sexpScript.sml so that examples/acl2/ml now builds.

acl2_packageScript: Fixed to run on the experimental kernel, now uses an iterative partitioning function and abbreviates long terms to keep execution time down.

translateScript: New acl2 definitions and rewrites for list definitions
acl2_packageScript: A bit faster again...

acl2_packageScript.sml: Modifed again to improve compile time, now O(n. log n) so probably as good as its going to get!

acl2_packageScript: Updated to compile faster

Defines and validates ACL2 package structure. Validation proof takes 8
hours! Tried to count the primitive inferences, but Count.apply
causes an overflow (see commented out code at end).