Remove TABs from examples

More translations complete, CASE_SPLIT_CONV performs type instantiation, termination condition for strings, marginal speed up.

Fixed problems with encode o decode = fix not completing for some termination cases when applied to nil

Types based upon finite maps encode correctly and simple functions from the opsem script translate.
Some of the script has been translated in fmapExample.sml, however, translations now require conditional translation on successful evalation.

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!

Final raft of compatlibility changes.

Modifications to allow the translation to run under PolyML.

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

encodeLib.sml,translateScript.sml : Modified to use 'natp' from hol_defaxioms

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: Now handles lambda abstractions and let syntax natively
Improved support for difficult recursion schemes (eg. DIV)
translateScript: Added translations for strings and characters
Definitions are now checked one by one to avoid the
'couldn't protect' error
sexp: Added support for 'let a = b and c = d in...' syntax

encodeLib.sml: Variables renamed to avoid restricted acl2 keywords

translateScript: Added a reduction for SUC (PRE a)
encodeLib: It's now possible to encoding HO functions such as FILTER, MAP etc... and re-use these in further definitions. Flattening these definitions into ACL2 is still unsupported however.

translateScript: Modified NAT_CASE to use PRE a, which translates to (+ a (- 1)) rather than nfix (+ a (- 1)) which occasionally introduced termination problems.
encodeLib: Fixed a few type inferences bugs associated with the changes in translateScript.

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: Now encodes theorems, also some minor improvements to type checking and resolving constraints, such as non-zero denominators for divide.
translateLib: A few minor changes, added an andl judgement

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

Tidying up. Note that acl2_defsTheory replaces basic_defaxiomsTheory.

Getting things to work with the new improved naming scheme.
(e.g. COMMON-LISP::= is now called common_lisp_equal rather than acl2_equal,
and definitions proviously named *_acl2_defun are now stored as *_def).

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

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.