--- a/src/HOL/Tools/etc/options Wed Sep 22 12:25:09 2021 +0200
+++ b/src/HOL/Tools/etc/options Wed Sep 22 12:41:40 2021 +0200
@@ -32,9 +32,6 @@
public option sledgehammer_timeout : int = 30
-- "provers will be interrupted after this time (in seconds)"
-public option vampire_noncommercial : string = "unknown"
- -- "status of Vampire activation for noncommercial use (yes, no, unknown)"
-
public option SystemOnTPTP : string = "http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply"
-- "URL for SystemOnTPTP service"