Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified sledgehammer options to approximate old-style diagnostic command;
authorwenzelm
Tue, 14 Apr 2015 22:50:11 +0200
changeset 60071 323feed18a92
parent 60070 73c6e58a105c
child 60072 dda1e781c7b4
clarified sledgehammer options to approximate old-style diagnostic command;
src/HOL/Tools/etc/options file | annotate | diff | comparison | revisions 
--- 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)"
isabelle