--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 24 22:57:22 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Aug 25 09:02:07 2010 +0200
@@ -452,10 +452,10 @@
relevance filter. The option ranges from 0 to 100, where 0 means that all
theorems are relevant.
-\opdefault{relevance\_convergence}{int}{31}
-Specifies the convergence factor, expressed as a percentage, used by the
-relevance filter. This factor is used by the relevance filter to scale down the
-relevance of facts at each iteration of the filter.
+\opdefault{relevance\_decay}{int}{31}
+Specifies the decay factor, expressed as a percentage, used by the relevance
+filter. This factor is used by the relevance filter to scale down the relevance
+of new facts at each iteration of the filter.
\opdefault{max\_relevant\_per\_iter}{int\_or\_smart}{\textit{smart}}
Specifies the maximum number of facts that may be added during one iteration of