enabled FOOL for Vampire in Sledgehammer
authordesharna
Wed, 22 Sep 2021 12:25:09 +0200
changeset 74351 d8dbe7525ff1
parent 74350 398b7bb9ebdd
child 74352 fb8ce6090437
enabled FOOL for Vampire in Sledgehammer
src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Sep 22 10:46:42 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Sep 22 12:25:09 2021 +0200
@@ -488,7 +488,7 @@
 
 val vampire_config : atp_config =
   let
-    val format = TFF (Without_FOOL, Monomorphic)
+    val format = TFF (With_FOOL, Monomorphic)
   in
     {exec = (["VAMPIRE_HOME"], ["vampire"]),
      arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ =>