--- a/doc-src/Sledgehammer/sledgehammer.tex Mon Aug 23 18:39:12 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Mon Aug 23 18:53:11 2010 +0200
@@ -452,9 +452,9 @@
relevance filter. The option ranges from 0 to 100, where 0 means that all
theorems are relevant.
-\opdefault{relevance\_convergence}{int}{320}
-Specifies the convergence quotient, multiplied by 100, used by the relevance
-filter. This quotient is used by the relevance filter to scale down the
+\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{max\_relevant\_per\_iter}{int\_or\_smart}{\textit{smart}}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 23 18:39:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 23 18:53:11 2010 +0200
@@ -335,7 +335,7 @@
val rel_const_tab =
rel_const_tab |> fold add_const_type_to_table new_consts
val threshold =
- threshold + (1.0 - threshold) / relevance_convergence
+ threshold + (1.0 - threshold) * relevance_convergence
in
trace_msg (fn () => "relevant this iteration: " ^
Int.toString (length newrels));
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 23 18:39:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 23 18:53:11 2010 +0200
@@ -68,7 +68,7 @@
("overlord", "false"),
("explicit_apply", "false"),
("relevance_threshold", "40"),
- ("relevance_convergence", "320"),
+ ("relevance_convergence", "31"),
("max_relevant_per_iter", "smart"),
("theory_relevant", "smart"),
("defs_relevant", "false"),