1signature m0_progLib =
2sig
3   val REG_CONV: Conv.conv
4   val addInstructionClass: string -> bool
5   val get_code: Thm.thm -> Term.term
6   val m0_config: bool -> string -> unit
7   val m0_introduction: Drule.rule
8   val m0_spec: string -> Thm.thm list
9   val m0_spec_code: string quotation -> Thm.thm list list
10   val m0_spec_hex: string -> Thm.thm list
11   val memory_introduction: Drule.rule
12   val mk_thumb2_pair: bool -> Term.term -> Term.term
13   val register_introduction: Drule.rule
14   val set_newline: string -> unit
15end
16