# HG changeset patch
# User blanchet
# Date 1304369535 -7200
# Node ID c7b71b55099bb57aa94a2d6d082062cbbd3db1a1
# Parent  f5b4b9d4acda69fa36f278c6bdd28c84a3e84a8c
better default type systems for SNARK and ToFoF

diff -r f5b4b9d4acda -r c7b71b55099b src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon May 02 22:52:15 2011 +0200
@@ -366,14 +366,14 @@
 val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"]
 val remote_tofof_e =
   remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
-             Conjecture [Tff] (K 200 (* FUDGE *)) []
+             Conjecture [Tff] (K 200 (* FUDGE *)) ["many_typed"]
 val remote_sine_e =
   remote_atp sine_eN "SInE" ["0.4"] [] [] Conjecture [Fof] (K 500 (* FUDGE *))
                      (#best_type_systems e_config)
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r024"]
              [("refutation.", "end_refutation.")] [] Conjecture [Tff, Fof]
-             (K 250 (* FUDGE *)) []
+             (K 250 (* FUDGE *)) ["many_typed"]
 
 (* Setup *)