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