src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 57037 c51132be8e16
parent 56985 82c83978fbd9
child 57054 fed0329ea8e2
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed May 21 13:52:46 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed May 21 14:09:42 2014 +0200
     1.3 @@ -67,6 +67,7 @@
     1.4      -> prover_problem -> prover_result
     1.5  
     1.6    val SledgehammerN : string
     1.7 +  val str_of_mode : mode -> string
     1.8    val smtN : string
     1.9    val overlord_file_location_of_prover : string -> string * string
    1.10    val proof_banner : mode -> string -> string
    1.11 @@ -104,12 +105,19 @@
    1.12  open Sledgehammer_Fact
    1.13  open Sledgehammer_Proof_Methods
    1.14  
    1.15 -datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
    1.16 -
    1.17  (* Identifier that distinguishes Sledgehammer from other tools that could use
    1.18     "Async_Manager". *)
    1.19  val SledgehammerN = "Sledgehammer"
    1.20  
    1.21 +datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
    1.22 +
    1.23 +fun str_of_mode Auto_Try = "Auto Try"
    1.24 +  | str_of_mode Try = "Try"
    1.25 +  | str_of_mode Normal = "Normal"
    1.26 +  | str_of_mode MaSh = "MaSh"
    1.27 +  | str_of_mode Auto_Minimize = "Auto_Minimize"
    1.28 +  | str_of_mode Minimize = "Minimize"
    1.29 +
    1.30  val smtN = "smt"
    1.31  
    1.32  val proof_method_names = [metisN, smtN]