--- 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 *}
--- 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