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