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