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!

Complete rework of the function encoding for ACL2. Usage of the encoding is
contained in acl2encodeLib.sig.

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.

encodeLib: Added two new modes of encoding functions, restricted, where the input domain is restricted (eg. ~(x = 0)), and recursive, where a recursive helper theorem is added to assist with termination in ACL2.

encodeLib: Complete re-vamp, can now do PolyTypism, however has limited support for case functions eg. NULL

translateScript: Now uses |= for type judgements, and makes use of some new functions such as andl and implies.

translateLib: Some functions to support encoding which are used in both encodeLib and translateScript

File: encodeLib.sml

Provides functions to encode HOL into ACL2

File: encodeLib.sig

Signature for encodeLib.sml

File: translateScript.sml

Provides translation theorems between HOL and the sexp type.
New constants are also defined here, which must be slurped along with anything
being encoded.