--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed May 15 22:02:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed May 15 22:30:24 2013 +0200
@@ -46,7 +46,10 @@
val _ =
ProofGeneral.preference_bool ProofGeneral.category_tracing
- auto "auto-sledgehammer" "Run Sledgehammer automatically"
+ NONE
+ auto
+ "auto-sledgehammer"
+ "Run Sledgehammer automatically"
(** Sledgehammer commands **)
@@ -66,12 +69,14 @@
val _ =
ProofGeneral.preference_string ProofGeneral.category_proof
+ NONE
provers
"Sledgehammer: Provers"
"Default automatic provers (separated by whitespace)"
val _ =
ProofGeneral.preference_int ProofGeneral.category_proof
+ NONE
timeout
"Sledgehammer: Time Limit"
"ATPs will be interrupted after this time (in seconds)"