src/HOL/Tools/res_atp_methods.ML
changeset 24215 5458fbf18276
parent 23590 ad95084a5c63
child 24300 e170cee91c66
     1.1 --- a/src/HOL/Tools/res_atp_methods.ML	Fri Aug 10 14:49:01 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp_methods.ML	Fri Aug 10 15:13:18 2007 +0200
     1.3 @@ -17,22 +17,22 @@
     1.4  
     1.5  (* vampire, eprover and spass tactics *)
     1.6  
     1.7 -fun vampire_tac st = res_atp_tac false vampire_oracle ResAtp.Auto (!ResAtp.vampire_time) st;
     1.8 -fun eprover_tac st = res_atp_tac false eprover_oracle ResAtp.Auto (!ResAtp.eprover_time) st;
     1.9 -fun spass_tac st = res_atp_tac true spass_oracle ResAtp.Auto (!ResAtp.spass_time) st;
    1.10 +fun vampire_tac st = res_atp_tac false vampire_oracle ResAtp.Auto (!ResAtp.time_limit) st;
    1.11 +fun eprover_tac st = res_atp_tac false eprover_oracle ResAtp.Auto (!ResAtp.time_limit) st;
    1.12 +fun spass_tac st = res_atp_tac true spass_oracle ResAtp.Auto (!ResAtp.time_limit) st;
    1.13  
    1.14  
    1.15 -fun vampireF_tac st = res_atp_tac false vampire_oracle ResAtp.Fol (!ResAtp.vampire_time) st;
    1.16 +fun vampireF_tac st = res_atp_tac false vampire_oracle ResAtp.Fol (!ResAtp.time_limit) st;
    1.17  
    1.18 -fun vampireH_tac st = res_atp_tac false vampire_oracle ResAtp.Hol (!ResAtp.vampire_time) st;
    1.19 +fun vampireH_tac st = res_atp_tac false vampire_oracle ResAtp.Hol (!ResAtp.time_limit) st;
    1.20  
    1.21 -fun eproverF_tac st = res_atp_tac false eprover_oracle ResAtp.Fol (!ResAtp.eprover_time) st;
    1.22 +fun eproverF_tac st = res_atp_tac false eprover_oracle ResAtp.Fol (!ResAtp.time_limit) st;
    1.23  
    1.24 -fun eproverH_tac st = res_atp_tac false eprover_oracle ResAtp.Hol (!ResAtp.eprover_time) st;
    1.25 +fun eproverH_tac st = res_atp_tac false eprover_oracle ResAtp.Hol (!ResAtp.time_limit) st;
    1.26  
    1.27 -fun spassF_tac st = res_atp_tac true spass_oracle ResAtp.Fol (!ResAtp.spass_time) st;
    1.28 +fun spassF_tac st = res_atp_tac true spass_oracle ResAtp.Fol (!ResAtp.time_limit) st;
    1.29  
    1.30 -fun spassH_tac st = res_atp_tac true spass_oracle ResAtp.Hol (!ResAtp.spass_time) st;
    1.31 +fun spassH_tac st = res_atp_tac true spass_oracle ResAtp.Hol (!ResAtp.time_limit) st;
    1.32  
    1.33  val ResAtps_setup =
    1.34    Method.add_methods