1signature lisp_extractLib =
2sig
3
4    include Abbrev
5
6    (* main functions for extraction *)
7
8    val pure_extract              : string -> tactic option -> thm
9    val pure_extract_mutual_rec   : string list -> tactic option -> thm
10    val impure_extract            : string -> tactic option -> thm
11    val impure_extract_cut        : string -> tactic option -> thm
12
13    (* function used for code synthesis *)
14
15    val deep_embeddings           : string -> (thm * thm) list -> thm * thm list
16
17    (* setting the state of the extractor *)
18
19    val set_lookup_thm    : thm -> unit
20    val install_assum_eq  : thm -> unit
21    val atbl_install      : string -> thm -> unit
22
23end
24