--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Sun Mar 28 18:39:27 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Mar 29 12:01:00 2010 +0200
@@ -14,9 +14,10 @@
verbose: bool,
atps: string list,
full_types: bool,
+ respect_no_atp: bool,
relevance_threshold: real,
+ convergence: real,
higher_order: bool option,
- respect_no_atp: bool,
follow_defs: bool,
isar_proof: bool,
timeout: Time.time,
@@ -56,15 +57,16 @@
(** parameters, problems, results, and provers **)
-(* TODO: "theory_const", "blacklist_filter", "convergence" *)
+(* TODO: "theory_const" *)
type params =
{debug: bool,
verbose: bool,
atps: string list,
full_types: bool,
+ respect_no_atp: bool,
relevance_threshold: real,
+ convergence: real,
higher_order: bool option,
- respect_no_atp: bool,
follow_defs: bool,
isar_proof: bool,
timeout: Time.time,