diff -r b49329185b82 -r dc6769b86fd6 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -43,6 +43,7 @@
 
   val agsyholN : string
   val alt_ergoN : string
+  val cvc4N : string
   val eN : string
   val iproverN : string
   val leo2N : string
@@ -50,7 +51,9 @@
   val satallaxN : string
   val spassN : string
   val vampireN : string
+  val veritN : string
   val waldmeisterN : string
+  val z3N : string
   val z3_tptpN : string
   val zipperpositionN : string
   val remote_prefix : string
@@ -107,6 +110,7 @@
 
 val agsyholN = "agsyhol"
 val alt_ergoN = "alt_ergo"
+val cvc4N = "cvc4"
 val eN = "e"
 val iproverN = "iprover"
 val leo2N = "leo2"
@@ -114,10 +118,13 @@
 val satallaxN = "satallax"
 val spassN = "spass"
 val vampireN = "vampire"
+val veritN = "verit"
 val waldmeisterN = "waldmeister"
+val z3N = "z3"
 val z3_tptpN = "z3_tptp"
 val zipperpositionN = "zipperposition"
 val remote_prefix = "remote_"
+
 val dummy_fofN = "dummy_fof"
 val dummy_tfxN = "dummy_tfx"
 val dummy_thfN = "dummy_thf"