--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 24 22:57:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 09:02:07 2010 +0200
@@ -68,7 +68,7 @@
("overlord", "false"),
("explicit_apply", "false"),
("relevance_threshold", "40"),
- ("relevance_convergence", "31"),
+ ("relevance_decay", "31"),
("max_relevant_per_iter", "smart"),
("theory_relevant", "smart"),
("defs_relevant", "false"),
@@ -170,8 +170,8 @@
val explicit_apply = lookup_bool "explicit_apply"
val relevance_threshold =
0.01 * Real.fromInt (lookup_int "relevance_threshold")
- val relevance_convergence =
- 0.01 * Real.fromInt (lookup_int "relevance_convergence")
+ val relevance_decay =
+ 0.01 * Real.fromInt (lookup_int "relevance_decay")
val max_relevant_per_iter = lookup_int_option "max_relevant_per_iter"
val theory_relevant = lookup_bool_option "theory_relevant"
val defs_relevant = lookup_bool "defs_relevant"
@@ -182,7 +182,7 @@
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
full_types = full_types, explicit_apply = explicit_apply,
relevance_threshold = relevance_threshold,
- relevance_convergence = relevance_convergence,
+ relevance_decay = relevance_decay,
max_relevant_per_iter = max_relevant_per_iter,
theory_relevant = theory_relevant, defs_relevant = defs_relevant,
isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,