--- a/src/HOL/Tools/etc/options Sun Jul 01 20:29:23 2018 +0100
+++ b/src/HOL/Tools/etc/options Mon Jul 02 10:02:44 2018 +0200
@@ -32,5 +32,8 @@
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 MaSh : string = "sml"
-- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"