clarified option name, with improved sort order wrt. "time" options;
authorwenzelm
Sat, 20 Jul 2013 16:45:00 +0200
changeset 52717 da7bf8b3d24a
parent 52716 ecb46f11c366
child 52718 0faf89b8d928
clarified option name, with improved sort order wrt. "time" options;
src/HOL/Tools/etc/options
src/HOL/Tools/try0.ML
--- 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;