added see also
authorblanchet
Fri, 20 May 2011 12:47:59 +0200
changeset 42888 4da581400b69
parent 42887 771be1dcfef6
child 42889 412fe70f41a4
added see also
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}