
diff -r 4e8a6354c54f -r e10f15652026 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Mar 01 08:00:51 2023 +0100
@@ -242,8 +242,7 @@
 e: Try this: \textbf{by} \textit{simp} (0.3 ms) \\
 cvc4: Try this: \textbf{by} \textit{simp} (0.4 ms) \\
 z3: Try this: \textbf{by} \textit{simp} (0.5 ms) \\
-vampire: Try this: \textbf{by} \textit{simp} (0.3 ms) \\
-Done
+vampire: Try this: \textbf{by} \textit{simp} (0.3 ms)
 \postw
 
 Sledgehammer ran CVC4, E, Vampire, Z3, and possibly other provers in parallel.
@@ -279,9 +278,15 @@
 \slshape
 vampire found an inconsistency\ldots \\
 vampire: The goal is inconsistent with these facts: append\_Cons, nth\_append\_length, self\_append\_conv2, zip\_eq\_Nil\_iff
-Done
 \postw
 
+Sometimes Sledgehammer will helpfully suggest a missing assumption:
+
+\prew
+\slshape
+e: Candidate for missing hypothesis: \\
+length ys = length xs
+\postw
 
 \section{Hints}
 \label{hints}
@@ -813,15 +818,27 @@
 \opnodefault{prover}{string}
 Alias for \textit{provers}.
 
-\opsmart{check\_consistent}{dont\_check\_consistent}
+\opsmart{check\_inconsistent}{dont\_check\_inconsistent}
 Specifies whether Sledgehammer should look for inconsistencies or for proofs. By
 default, it looks for both proofs and inconsistencies.
 
 An inconsistency indicates that the goal, taken as an axiom, would be
 inconsistent with some specific background facts if it were added as a lemma,
 indicating a likely issue with the goal. Sometimes the inconsistency involves
-only the background theory; this might happen, for example, if an axiom is used
-or if a lemma was introduced with \textbf{sorry}.
+only the background theory; this might happen, for example, if a flawed axiom is
+used or if a flawed lemma was introduced with \textbf{sorry}.
+
+\opdefault{abduce}{smart\_int}{smart}
+Specifies the maximum number of candidate missing hypotheses that may be
+displayed. These hypotheses are discovered heuristically by a process called
+abduction (as opposed to deduction)---that is, they are guessed and found to be
+sufficient to prove the goal.
+
+Abduction is currently supported only by E. If the option is set to
+\textit{smart} (the default), abduction is enabled only in some of the E time
+slices, and only one candidate missing hypothesis is displayed. You can disable
+abduction altogether by setting the option to 0 or enable it in all time slices
+by setting it to a nonzero value.
 
 \optrue{minimize}{dont\_minimize}
 Specifies whether the proof minimization tool should be invoked automatically




