--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri May 14 15:27:07 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri May 14 16:15:10 2010 +0200
@@ -20,9 +20,9 @@
explicit_apply: bool,
respect_no_atp: bool,
relevance_threshold: real,
- convergence: real,
+ relevance_convergence: real,
theory_relevant: bool option,
- follow_defs: bool,
+ defs_relevant: bool,
isar_proof: bool,
shrink_factor: int,
timeout: Time.time,
@@ -79,9 +79,9 @@
explicit_apply: bool,
respect_no_atp: bool,
relevance_threshold: real,
- convergence: real,
+ relevance_convergence: real,
theory_relevant: bool option,
- follow_defs: bool,
+ defs_relevant: bool,
isar_proof: bool,
shrink_factor: int,
timeout: Time.time,