# HG changeset patch
# User blanchet
# Date 1677654051 -3600
# Node ID 73611eb994cff796d032c25f792f6e6a43ad87de
# Parent  779faa014564458c7a334a9686e7336c679efb5f
slightly more documentation

diff -r 779faa014564 -r 73611eb994cf 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
@@ -818,7 +818,7 @@
 \opnodefault{prover}{string}
 Alias for \textit{provers}.
 
-\opsmart{check\_inconsistent}{dont\_check\_inconsistent}
+\opsmartx{check\_inconsistent}{dont\_check\_inconsistent}
 Specifies whether Sledgehammer should look for inconsistencies or for proofs. By
 default, it looks for both proofs and inconsistencies.
 
@@ -831,8 +831,8 @@
 \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 (which stands in contrast 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
@@ -840,6 +840,9 @@
 abduction altogether by setting the option to 0 or enable it in all time slices
 by setting it to a nonzero value.
 
+\optrueonly{dont\_abduce}
+Alias for ``\textit{abduce} = 0''.
+
 \optrue{minimize}{dont\_minimize}
 Specifies whether the proof minimization tool should be invoked automatically
 after proof search.