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