tuned method description
authorblanchet
Thu Aug 28 16:58:26 2014 +0200 (2014-08-28)
changeset 58072a86c962de77f
parent 58071 62ec5b1d2f2f
child 58073 1cd45fec98e2
tuned method description
src/HOL/SMT.thy
src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
     1.1 --- a/src/HOL/SMT.thy	Thu Aug 28 16:58:26 2014 +0200
     1.2 +++ b/src/HOL/SMT.thy	Thu Aug 28 16:58:26 2014 +0200
     1.3 @@ -127,7 +127,7 @@
     1.4    Scan.optional Attrib.thms [] >>
     1.5      (fn thms => fn ctxt =>
     1.6        METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts))))
     1.7 -*} "apply an SMT solver to the current goal (based on SMT-LIB 2)"
     1.8 +*} "apply an SMT solver to the current goal"
     1.9  
    1.10  
    1.11  subsection {* Configuration *}
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Aug 28 16:58:26 2014 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Aug 28 16:58:26 2014 +0200
     2.3 @@ -32,6 +32,7 @@
     2.4    type one_line_params =
     2.5      ((string * stature) list * (proof_method * play_outcome)) * string * int * int
     2.6  
     2.7 +  val skolemize_tac : Proof.context -> int -> tactic
     2.8    val is_proof_method_direct : proof_method -> bool
     2.9    val string_of_proof_method : Proof.context -> string list -> proof_method -> string
    2.10    val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic