src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 36059 ab3dfdeb9603
parent 36058 8256d5a185bd
child 36063 cdc6855a6387
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Mar 29 12:01:00 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Mar 29 12:21:51 2010 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4       respect_no_atp: bool,
     1.5       relevance_threshold: real,
     1.6       convergence: real,
     1.7 +     theory_const: bool option,
     1.8       higher_order: bool option,
     1.9       follow_defs: bool,
    1.10       isar_proof: bool,
    1.11 @@ -57,7 +58,6 @@
    1.12  
    1.13  (** parameters, problems, results, and provers **)
    1.14  
    1.15 -(* TODO: "theory_const" *)
    1.16  type params =
    1.17    {debug: bool,
    1.18     verbose: bool,
    1.19 @@ -66,6 +66,7 @@
    1.20     respect_no_atp: bool,
    1.21     relevance_threshold: real,
    1.22     convergence: real,
    1.23 +   theory_const: bool option,
    1.24     higher_order: bool option,
    1.25     follow_defs: bool,
    1.26     isar_proof: bool,