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