--- a/src/Doc/Sledgehammer/document/root.tex Thu May 22 03:29:35 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu May 22 03:29:35 2014 +0200
@@ -269,24 +269,19 @@
\prew
\slshape
-Sledgehammer: ``\textit{e\/}'' on goal \\
-$[a] = [b] \,\Longrightarrow\, a = b$ \\
+Sledgehammer: ``\textit{e\/}'' \\
Try this: \textbf{by} (\textit{metis last\_ConsL}) (64 ms). \\[3\smallskipamount]
%
-Sledgehammer: ``\textit{z3\/}'' on goal \\
-$[a] = [b] \,\Longrightarrow\, a = b$ \\
+Sledgehammer: ``\textit{z3\/}'' \\
Try this: \textbf{by} (\textit{metis list.inject}) (20 ms). \\[3\smallskipamount]
%
-Sledgehammer: ``\textit{vampire\/}'' on goal \\
-$[a] = [b] \,\Longrightarrow\, a = b$ \\
+Sledgehammer: ``\textit{vampire\/}'' \\
Try this: \textbf{by} (\textit{metis hd.simps}) (14 ms). \\[3\smallskipamount]
%
-Sledgehammer: ``\textit{spass\/}'' on goal \\
-$[a] = [b] \,\Longrightarrow\, a = b$ \\
+Sledgehammer: ``\textit{spass\/}'' \\
Try this: \textbf{by} (\textit{metis list.inject}) (17 ms). \\[3\smallskipamount]
%
-Sledgehammer: ``\textit{remote\_e\_sine\/}'' on goal \\
-$[a] = [b] \,\Longrightarrow\, a = b$ \\
+Sledgehammer: ``\textit{remote\_e\_sine\/}'' \\
Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms).
\postw
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu May 22 03:29:35 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu May 22 03:29:35 2014 +0200
@@ -54,15 +54,9 @@
ordered_outcome_codes
|> the_default unknownN
-fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i n goal =
+fun prover_description verbose name num_facts =
(quote name,
- (if verbose then
- " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
- else
- "") ^
- " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
- (if blocking then "."
- else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
+ if verbose then " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts else "")
fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...}) mode
output_result minimize_command only learn
@@ -77,8 +71,6 @@
val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
val num_facts = length facts |> not only ? Integer.min max_facts
- fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal
-
val problem =
{comment = comment, state = state, goal = goal, subgoal = subgoal,
subgoal_count = subgoal_count,
@@ -195,7 +187,8 @@
|> List.app Output.urgent_message
in (outcome_code, state) end
else
- (Async_Manager.thread SledgehammerN birth_time death_time (desc ())
+ (Async_Manager.thread SledgehammerN birth_time death_time
+ (prover_description verbose name num_facts)
((fn (outcome_code, message) => (verbose orelse outcome_code = someN, message ())) o go);
(unknownN, state))
end