1signature core_decompilerLib = 2sig 3 4 val code_parser: (string quotation -> string list) option ref 5 6 val configure: {pc_tm: Term.term, 7 init_fn: unit -> unit, 8 pc_conv: Conv.conv -> Conv.conv, 9 triple_fn: string -> helperLib.instruction, 10 component_vars: Term.term list} -> unit 11 12 val core_decompile: string -> string quotation -> Thm.thm * Thm.thm 13 14 val compose : Thm.thm -> Thm.thm -> Thm.thm 15 16end 17