src/HOL/Tools/ATP/atp_systems.ML
changeset 40344 df25b51af013
parent 40060 5ef6747aa619
child 40426 339f56417109
equal deleted inserted replaced
40343:4521d56aef63 40344:df25b51af013
    78 fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000
    78 fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000
    79 
    79 
    80 
    80 
    81 (* E *)
    81 (* E *)
    82 
    82 
    83 (* Give older versions of E an extra second, because the "eproof" script wrongly
    83 (* Give E an extra second to reconstruct the proof. Older versions even get two
    84    subtracted an entire second to account for the overhead of the script
    84    seconds, because the "eproof" script wrongly subtracted an entire second to
    85    itself, which is in fact much lower. *)
    85    account for the overhead of the script itself, which is in fact much
       
    86    lower. *)
    86 fun e_bonus () =
    87 fun e_bonus () =
    87   case getenv "E_VERSION" of
    88   case getenv "E_VERSION" of
    88     "" => 1000
    89     "" => 2000
    89   | version =>
    90   | version =>
    90     if exists (fn s => String.isPrefix s version) ["0.9", "1.0"] then 1000
    91     if exists (fn s => String.isPrefix s version) ["0.9", "1.0"] then 2000
    91     else 0
    92     else 1000
    92 
    93 
    93 val tstp_proof_delims =
    94 val tstp_proof_delims =
    94   ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
    95   ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
    95 
    96 
    96 val e_config : atp_config =
    97 val e_config : atp_config =