1signature arm8_stepLib =
2sig
3   val arm8_decode: Term.term -> Thm.thm
4   val arm8_decode_hex: string -> Thm.thm
5   val arm8_decode_instruction: string -> Thm.thm
6   val arm8_instruction: Term.term -> string option
7   val arm8_names: string list
8   val arm8_pattern: string -> Term.term option
9   val arm8_step: Term.term -> Thm.thm list
10   val arm8_step_code: string quotation -> Thm.thm list list
11   val arm8_step_hex: string -> Thm.thm list
12
13   val ARM8_CONV: Conv.conv
14   val DATATYPE_CONV: Conv.conv
15   val REG_31_RULE: Drule.rule
16end
17