# HG changeset patch
# User blanchet
# Date 1409237906 -7200
# Node ID a86c962de77f9da7ca07302d675bf0a2dea19396
# Parent  62ec5b1d2f2fee56fa201886f3181acddc1dcbd4
tuned method description

diff -r 62ec5b1d2f2f -r a86c962de77f src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Thu Aug 28 16:58:26 2014 +0200
+++ b/src/HOL/SMT.thy	Thu Aug 28 16:58:26 2014 +0200
@@ -127,7 +127,7 @@
   Scan.optional Attrib.thms [] >>
     (fn thms => fn ctxt =>
       METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts))))
-*} "apply an SMT solver to the current goal (based on SMT-LIB 2)"
+*} "apply an SMT solver to the current goal"
 
 
 subsection {* Configuration *}
diff -r 62ec5b1d2f2f -r a86c962de77f src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Aug 28 16:58:26 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Aug 28 16:58:26 2014 +0200
@@ -32,6 +32,7 @@
   type one_line_params =
     ((string * stature) list * (proof_method * play_outcome)) * string * int * int
 
+  val skolemize_tac : Proof.context -> int -> tactic
   val is_proof_method_direct : proof_method -> bool
   val string_of_proof_method : Proof.context -> string list -> proof_method -> string
   val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic