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