Remove eqtype declaration for term type

Some function in bitstringSyntax are now based on Arbnum.num instead of Int.int.

The old versions were vulnerable to Overflow exceptions.

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.

Add a bit-string rotate operation.

A better error message for bitstringSyntax.bitstring_of_hexstring.

Add assembly code parsing/printing support for the M0 and ARMv7 models.

There are new entry points to the decompiler. These take a function that maps a quotation (containing machine or assembly code) into a list of strings (typically hex). This facilitate the input of ARM assembly code. For example, the functions:

m0_decompLib.m0_decompile_code
m0_core_decompLib.m0_core_decompile_code
arm_decompLib.arm_decompile_code
arm_core_decompLib.arm_core_decompile_code

are provided with type

: string -> string quotation -> Thm.thm * Thm.thm

Add a few more functions to bitstringSyntax.

Update some syntax files to use HolKernel.syntax_fns.

Add a theory of bit-strings, which defines word operations over ``:bool list``. The maps "v2w" and "w2v" provide a connection to fixed-width bit vectors.