# HG changeset patch
# User wenzelm
# Date 1373717508 -7200
# Node ID e8c1c561267706fb2fd5ad4b9a6e8258ce874575
# Parent  cea207576f8132c29043f700ca327466170bf7df
clarified some default options;

diff -r cea207576f81 -r e8c1c5612677 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Sat Jul 13 13:58:13 2013 +0200
+++ b/src/HOL/Tools/etc/options	Sat Jul 13 14:11:48 2013 +0200
@@ -2,7 +2,7 @@
 
 section {* Isabelle/HOL proof tools *}
 
-public option auto_time_limit : real = 4.0
+public option auto_time_limit : real = 2.0
   -- "time limit for automatically tried tools (seconds > 0)"
 
 public option auto_nitpick : bool = false
@@ -14,9 +14,9 @@
 public option auto_try0 : bool = false
   -- "try standard proof methods automatically"
 
-public option auto_quickcheck : bool = false
+public option auto_quickcheck : bool = true
   -- "run Quickcheck automatically"
 
-public option auto_solve_direct : bool = false
+public option auto_solve_direct : bool = true
   -- "run solve_direct automatically"
 
diff -r cea207576f81 -r e8c1c5612677 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Sat Jul 13 13:58:13 2013 +0200
+++ b/src/Tools/quickcheck.ML	Sat Jul 13 14:11:48 2013 +0200
@@ -94,7 +94,7 @@
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
-    (SOME "true")
+    NONE
     @{option auto_quickcheck}
     "auto-quickcheck"
     "Run Quickcheck automatically";
diff -r cea207576f81 -r e8c1c5612677 src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Sat Jul 13 13:58:13 2013 +0200
+++ b/src/Tools/solve_direct.ML	Sat Jul 13 14:11:48 2013 +0200
@@ -35,7 +35,7 @@
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
-    (SOME "true")
+    NONE
     @{option auto_solve_direct}
     "auto-solve-direct"
     ("Run " ^ quote solve_directN ^ " automatically");
diff -r cea207576f81 -r e8c1c5612677 src/Tools/try.ML
--- a/src/Tools/try.ML	Sat Jul 13 13:58:13 2013 +0200
+++ b/src/Tools/try.ML	Sat Jul 13 14:11:48 2013 +0200
@@ -31,7 +31,7 @@
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
-    NONE
+    (SOME "4.0")
     @{option auto_time_limit}
     "auto-try-time-limit"
     "Time limit for automatically tried tools (in seconds)"