# HG changeset patch
# User wenzelm
# Date 1429044611 -7200
# Node ID 323feed18a92fec873c0b6d47b256e4c01cfe942
# Parent  73c6e58a105c2c28376ad292796ba65f7e4655a2
clarified sledgehammer options to approximate old-style diagnostic command;

diff -r 73c6e58a105c -r 323feed18a92 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Tue Apr 14 16:47:55 2015 +0200
+++ b/src/HOL/Tools/etc/options	Tue Apr 14 22:50:11 2015 +0200
@@ -26,11 +26,11 @@
 
 section "Miscellaneous Tools"
 
-public option sledgehammer_provers : string = "e spass remote_vampire"
-  -- "ATPs for Sledgehammer (separated by blanks)"
+public option sledgehammer_provers : string = "cvc4 remote_vampire z3 spass e"
+  -- "provers for Sledgehammer (separated by blanks)"
 
 public option sledgehammer_timeout : int = 30
-  -- "ATPs will be interrupted after this time (in seconds)"
+  -- "provers will be interrupted after this time (in seconds)"
 
 public option MaSh : string = "sml"
   -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"