# HG changeset patch
# User blanchet
# Date 1464019485 -7200
# Node ID 32492105b015ca51e3ddc60be3ee822e0bff523e
# Parent  39dca48916014791aa63cab1f2872a67d0194dcb
generate Vampire 4.0 compatible output

diff -r 39dca4891601 -r 32492105b015 NEWS
--- a/NEWS	Mon May 23 15:46:30 2016 +0100
+++ b/NEWS	Mon May 23 18:04:45 2016 +0200
@@ -95,6 +95,9 @@
 has been removed for output. It is retained for input only, until it is
 eliminated altogether.
 
+* Sledgehammer:
+  - Produce syntactically correct Vampire 4.0 problem files.
+
 * (Co)datatype package:
   - New commands for defining corecursive functions and reasoning about
     them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',
diff -r 39dca4891601 -r 32492105b015 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon May 23 15:46:30 2016 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon May 23 18:04:45 2016 +0200
@@ -532,7 +532,7 @@
       (Unprovable, "Termination reason: Satisfiable"),
       (Interrupted, "Aborted by signal SIGINT")] @
      known_szs_status_failures,
-   prem_role = Conjecture,
+   prem_role = Hypothesis,
    best_slices = fn ctxt =>
      (* FUDGE *)
      (if is_vampire_beyond_1_8 () then
@@ -724,7 +724,7 @@
   remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
     (K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
 val remote_vampire =
-  remotify_atp vampire "Vampire" ["3.0", "2.6", "2.5"]
+  remotify_atp vampire "Vampire" ["4.0", "3.0", "2.6"]
     (K (((400, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *))
 val remote_e_sine =
   remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture