clarified option name, with improved sort order wrt. "time" options;
--- a/src/HOL/Tools/etc/options Sat Jul 20 16:29:06 2013 +0200
+++ b/src/HOL/Tools/etc/options Sat Jul 20 16:45:00 2013 +0200
@@ -14,7 +14,7 @@
public option auto_sledgehammer : bool = false
-- "run Sledgehammer automatically"
-public option auto_try0 : bool = false
+public option auto_methods : bool = false
-- "try standard proof methods automatically"
public option auto_quickcheck : bool = true
--- a/src/HOL/Tools/try0.ML Sat Jul 20 16:29:06 2013 +0200
+++ b/src/HOL/Tools/try0.ML Sat Jul 20 16:45:00 2013 +0200
@@ -25,7 +25,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- @{option auto_try0}
+ @{option auto_methods}
"auto-try0"
"Try standard proof methods"
@@ -191,6 +191,6 @@
fun try_try0 auto =
do_try0 (if auto then Auto_Try else Try) NONE ([], [], [], [])
-val _ = Try.tool_setup (try0N, (30, @{option auto_try0}, try_try0))
+val _ = Try.tool_setup (try0N, (30, @{option auto_methods}, try_try0))
end;