Improving naming of bit-vector signed division constants.

This renaming introduces incompatibilities:

• words$word_sdiv -> words$word_quot (this is proved to be related to int_quot for a non-zero divisor).
• words$word_srem -> words$word_rem (this is proved to be related to int_rem for a non-zero divisor).
• integer_word$word_sdiv (this is a new constant defined directly in terms of int_div).
• words$word_smod -> integer_word$word_smod (this is now defined directly in terms of int_mod).

Modify the type of HolKernel.syntax_fns and add some documentation.

This is in response to issue #247.

The change to the type makes things a little more natural when using partial applications - for example, HolKernel.syntax_fns1 can be used to provide syntax support for regular unary operations.

Update some syntax files to use HolKernel.syntax_fns.

Add toString and fromString to integer_wordTheory. Also, make improvements to syntax files.

Added new definitions and theorems for various bit-vector "saturation"
operations.

These operations return maximal or minimal values instead of, e.g.,
overflowing (wrapping). For example:

|- signed_saturate_add 100w 50w = 127w: thm

Also added a new configuration option for printing word literals as 2's
complement values. For example:

> set_trace "word pp as 2's comp" 1;
> ``253w:word8``;
val it = ``-3w``: term

Be warned that this term is actually ``n2w 253``, it's just being printed as
``word_2comp (n2w 3)``.

This printing mode is useful when checking the veracity of machine arithmetic.
For example:

> EVAL ``signed_saturate_sub 226w 100w : word8``;
val it = |- signed_saturate_sub -30w 100w = -128w: thm

Syntax support for integer_word.