# HG changeset patch # User blanchet # Date 1369119778 -7200 # Node ID f353fe3c2b92cb883bdd9cc4ebaabf1936a56133 # Parent 7e9cd79e25b3eeec2d5a7984e8e304d16492ecf0 disabled choice in Satallax diff -r 7e9cd79e25b3 -r f353fe3c2b92 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue May 21 09:02:58 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue May 21 09:02:58 2013 +0200 @@ -485,8 +485,9 @@ (* Satallax *) +(* Choice is disabled until there is proper reconstruction for it. *) val satallax_thf0 = - THF (Monomorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs) + THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_With_Defs) val satallax_config : atp_config = {exec = (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),