--- a/src/HOL/Sledgehammer.thy Mon Jun 16 19:41:00 2014 +0200
+++ b/src/HOL/Sledgehammer.thy Mon Jun 16 19:41:01 2014 +0200
@@ -34,7 +34,7 @@
ML_file "Tools/Sledgehammer/sledgehammer_commands.ML"
lemma "1 + 1 = (2::nat)"
-sledgehammer [vampire, max_facts = 3]
+sledgehammer [remote_waldmeister, max_facts = 3, verbose, overlord]
oops
end
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 16 19:41:00 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 16 19:41:01 2014 +0200
@@ -718,11 +718,11 @@
remotify_config system_name system_versions best_slice o config)
fun gen_remote_waldmeister name =
- remote_atp name "Waldmeister" ["710"]
- [("#START OF PROOF", "Proved Goals:")]
- [(OutOfResources, "Too many function symbols"),
- (Inappropriate, "**** Unexpected end of file."),
- (Crashed, "Unrecoverable Segmentation Fault")]
+ remote_atp name "Waldmeister" ["710"] tstp_proof_delims
+ ([(OutOfResources, "Too many function symbols"),
+ (Inappropriate, "**** Unexpected end of file."),
+ (Crashed, "Unrecoverable Segmentation Fault")]
+ @ known_szs_status_failures)
Hypothesis
(K (((50, ""), CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *))