# HG changeset patch
# User blanchet
# Date 1305888479 -7200
# Node ID 4da581400b6982ab4dafb93b20b37f253ec52b40
# Parent  771be1dcfef6f66a57d5d4b6567fdc85add10002
added see also

diff -r 771be1dcfef6 -r 4da581400b69 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}