# HG changeset patch
# User blanchet
# Date 1282582391 -7200
# Node ID e2c04af9469bda4a363f115a4c0f79ea3710c99e
# Parent  23266607cb81dab39099e0a1affd3236b7fe5bf2
invert semantics of "relevance_convergence", to make it more intuitive

diff -r 23266607cb81 -r e2c04af9469b doc-src/Sledgehammer/sledgehammer.tex
--- 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}}
diff -r 23266607cb81 -r e2c04af9469b src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- 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));
diff -r 23266607cb81 -r e2c04af9469b src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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"),