--- 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',
--- 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