1signature arm_stepLib =
2sig
3   val BIT_THMS_CONV: Conv.conv
4   val arm_eval: string -> bool list * Term.term -> Thm.thm
5   val arm_instruction: Term.term list -> string list
6   val arm_step: string -> string -> Thm.thm list
7   val arm_step_code: string -> string quotation -> Thm.thm list list
8   val arm_step_hex: string -> string -> Thm.thm list
9   val arm_decode: Term.term list -> bool list * Term.term -> Thm.thm list
10   val arm_decode_hex: string -> string -> Thm.thm list
11   val hex_to_bits_32: string -> Term.term list
12   val list_instructions: unit -> string list
13   val print_instructions: unit -> unit
14
15   (*
16
17     open arm_stepLib
18     val () = print_instructions ()
19     val ev = arm_step "v7,vfp"
20     fun pev s = (print (s ^ "\n"); Count.apply ev s);
21     val _ = Count.apply (List.map ev) (list_instructions ())
22     val _ = Count.apply (List.map (Lib.total pev)) (list_instructions ())
23     ev "LDR (+reg,pre)"
24
25   *)
26end
27