doc-src/Sledgehammer/sledgehammer.tex

--- a/doc-src/Sledgehammer/sledgehammer.tex	Fri May 20 12:47:59 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri May 20 12:47:59 2011 +0200
@@ -885,6 +885,10 @@
 
 For SMT solvers and ToFoF-E, the type system is always \textit{simple},
 irrespective of the value of this option.
+
+\nopagebreak
+{\small See also \textit{max\_new\_mono\_instances} (\S\ref{relevance-filter})
+and \textit{max\_mono\_iters} (\S\ref{relevance-filter}).}
 \end{enum}
 
 \subsection{Relevance Filter}