src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 55323 253a029335a2
parent 55308 dc68f6fb88d2
child 55345 8a53ee72e595
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Tue Feb 04 21:29:46 2014 +0000
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Tue Feb 04 23:11:18 2014 +0100
     1.3 @@ -67,6 +67,7 @@
     1.4      -> prover_problem -> prover_result
     1.5  
     1.6    val SledgehammerN : string
     1.7 +  val smtN : string
     1.8    val overlord_file_location_of_prover : string -> string * string
     1.9    val proof_banner : mode -> string -> string
    1.10    val extract_proof_method : params -> proof_method -> string * (string * string list) list
    1.11 @@ -110,6 +111,8 @@
    1.12     "Async_Manager". *)
    1.13  val SledgehammerN = "Sledgehammer"
    1.14  
    1.15 +val smtN = "smt"
    1.16 +
    1.17  val proof_method_names = [metisN, smtN]
    1.18  val is_proof_method = member (op =) proof_method_names
    1.19