use right delimiters for Waldmeister proofs
authorblanchet
Mon, 16 Jun 2014 19:41:01 +0200
changeset 57265 cab38f7a3adb
parent 57264 13db1d078743
child 57266 6a3b5085fb8f
use right delimiters for Waldmeister proofs
src/HOL/Sledgehammer.thy
src/HOL/Tools/ATP/atp_systems.ML
--- 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 *))