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.

encodeLib: Major rewrite to allow encoding of functions with partial specifications.
translateScript: Extra theorems added for better resolution of natural numbers
testEncode: Updated to test partial specifications and some extra red-black tree examples added.

testEncode: Tests for native let handling added

testEncode: Added some tests for the HO function encoding

testEncode: Added examples of encoding with an added recursion theorem (log2) and a restricted input domain (modexp)

testEncode.sml Added a test for converting a theorem, DIVISION.

testEncode: Modifed to use the new encodeLib, Matt's example is now the original example, and hences uses polytypism. Some tests of encoding types have also been included, as well as some more interesting encodings, eg. Red-Black trees.

encodeLib.sml: Now includes a short pre-processing step to remove lambda abstractions and let expressions
testEncode.sml: Removed the simplification as its included in the above

testEncode.sml: Tests encoding of some simple arithmetic functions, and some load / store definitions due to Matt Kaufmann.