# HG changeset patch
# User blanchet
# Date 1277481781 -7200
# Node ID f329e1b99ce6780cdf27259542d76d8ab3f9c1c5
# Parent  03edc498db6f8de8fbda7676644b3d8bc49a0cca
update docs

diff -r 03edc498db6f -r f329e1b99ce6 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Fri Jun 25 17:32:55 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri Jun 25 18:03:01 2010 +0200
@@ -448,13 +448,6 @@
 should be considered particularly relevant. Enabling this option tends to lead
 to larger problems and typically slows down the ATPs.
 
-\optrue{respect\_no\_atp}{ignore\_no\_atp}
-Specifies whether Sledgehammer should honor the \textit{no\_atp} attributes. The
-\textit{no\_atp} attributes marks theorems that tend to confuse ATPs, typically
-because they can lead to unsound ATP proofs \cite{boehme-nipkow-2010}. It is
-normally a good idea to leave this option enabled, unless you are debugging
-Sledgehammer.
-
 \end{enum}
 
 \subsection{Output Format}