--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Jun 11 11:28:46 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Jun 11 15:29:23 2014 +0200
@@ -59,6 +59,7 @@
val spass_pirateN : string
val vampireN : string
val waldmeisterN : string
+ val waldmeister_newN : string
val z3_tptpN : string
val zipperpositionN : string
val remote_prefix : string
@@ -112,11 +113,11 @@
val spass_pirateN = "spass_pirate"
val vampireN = "vampire"
val waldmeisterN = "waldmeister"
+val waldmeister_newN = "waldmeister_new"
val z3_tptpN = "z3_tptp"
val zipperpositionN = "zipperposition"
val remote_prefix = "remote_"
-
val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *)
val satallax_core_rule = "__satallax_core" (* arbitrary *)
val spass_input_rule = "Inp"