src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 36058 8256d5a185bd
parent 35969 c9565298df9e
child 36059 ab3dfdeb9603
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sun Mar 28 18:39:27 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Mar 29 12:01:00 2010 +0200
     1.3 @@ -14,9 +14,10 @@
     1.4       verbose: bool,
     1.5       atps: string list,
     1.6       full_types: bool,
     1.7 +     respect_no_atp: bool,
     1.8       relevance_threshold: real,
     1.9 +     convergence: real,
    1.10       higher_order: bool option,
    1.11 -     respect_no_atp: bool,
    1.12       follow_defs: bool,
    1.13       isar_proof: bool,
    1.14       timeout: Time.time,
    1.15 @@ -56,15 +57,16 @@
    1.16  
    1.17  (** parameters, problems, results, and provers **)
    1.18  
    1.19 -(* TODO: "theory_const", "blacklist_filter", "convergence" *)
    1.20 +(* TODO: "theory_const" *)
    1.21  type params =
    1.22    {debug: bool,
    1.23     verbose: bool,
    1.24     atps: string list,
    1.25     full_types: bool,
    1.26 +   respect_no_atp: bool,
    1.27     relevance_threshold: real,
    1.28 +   convergence: real,
    1.29     higher_order: bool option,
    1.30 -   respect_no_atp: bool,
    1.31     follow_defs: bool,
    1.32     isar_proof: bool,
    1.33     timeout: Time.time,