# HG changeset patch
# User wenzelm
# Date 1374331500 -7200
# Node ID da7bf8b3d24a1b6e095f0d791675128c22c3d20b
# Parent  ecb46f11c366f1ca42d0ee61753977c68c6feeb4
clarified option name, with improved sort order wrt. "time" options;

diff -r ecb46f11c366 -r da7bf8b3d24a src/HOL/Tools/etc/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
diff -r ecb46f11c366 -r da7bf8b3d24a src/HOL/Tools/try0.ML
--- 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;