better default type systems for SNARK and ToFoF
authorblanchet
Mon, 02 May 2011 22:52:15 +0200
changeset 43514c7b71b55099b
parent 43513 f5b4b9d4acda
child 43515 9dd98edd48c2
better default type systems for SNARK and ToFoF
src/HOL/Tools/ATP/atp_systems.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Mon May 02 22:52:15 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon May 02 22:52:15 2011 +0200
     1.3 @@ -366,14 +366,14 @@
     1.4  val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"]
     1.5  val remote_tofof_e =
     1.6    remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
     1.7 -             Conjecture [Tff] (K 200 (* FUDGE *)) []
     1.8 +             Conjecture [Tff] (K 200 (* FUDGE *)) ["many_typed"]
     1.9  val remote_sine_e =
    1.10    remote_atp sine_eN "SInE" ["0.4"] [] [] Conjecture [Fof] (K 500 (* FUDGE *))
    1.11                       (#best_type_systems e_config)
    1.12  val remote_snark =
    1.13    remote_atp snarkN "SNARK" ["20080805r024"]
    1.14               [("refutation.", "end_refutation.")] [] Conjecture [Tff, Fof]
    1.15 -             (K 250 (* FUDGE *)) []
    1.16 +             (K 250 (* FUDGE *)) ["many_typed"]
    1.17  
    1.18  (* Setup *)
    1.19