Fix type of dest_update_comb.

Add dest_update_comb and is_update_comb to combinSyntax.

Add combinSyntax.strip_update. For example:

> combinSyntax.strip_update ``(a =+ x) ((b =+ y) ((c =+ z) f))``;
<<HOL message: inventing new type variable names: 'a, 'b>>
val it =
([(``a``, ``x``),
(``b``, ``y``),
(``c``, ``z``)], ``f``)
: (term * term) list * term

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!

Add UPDATE (=+) to combinSyntax.

Mostly minor changes. Mainly, have changed FUPDATE_LIST in
finite_mapTheory to be a prefix, and have replaced it with
the infix notation |++.

Michael said it was OK.

Added new combinator called FAIL, which is equal to K. FAIL is used
to generate exception-raising code when translated to ML. For
example

HD [] = FAIL HD ^(mk_var("Empty list",bool)) []

which is provable since FAIL x y = x. The translator to ML
will convert FAIL terms so that the above is

HD [] = raise Fail "HD: Empty list"

Many small changes, most associated with boolification or lifting.

Syntax for combinators.